%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWB024+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 : n032.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:15:55 PM UTC 2025
% Result : CounterSatisfiable 13.07s 4.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : SWB024+4 : TPTP v9.0.0. Released v5.2.0.
% 0.05/0.10 % 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.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Wed Apr 9 01:02:00 EDT 2025
% 0.10/0.29 % CPUTime :
% 13.07/4.40
% 13.07/4.40 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.07/4.40
% 13.07/4.40 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.07/4.41 %$ iext > icext > lv > ir > ip > ic > literal_typed > #nlpp > uri_xsd_nonNegativeInteger > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_onProperty > uri_owl_minCardinality > uri_owl_TransitiveProperty > uri_owl_Restriction > uri_ex_hasAncestor > uri_ex_bob > uri_ex_alice > uri_ex_Person > dat_str_1 > #skF_1
% 13.07/4.41
% 13.07/4.41 %Foreground sorts:
% 13.07/4.41
% 13.07/4.41
% 13.07/4.41 %Background operators:
% 13.07/4.41
% 13.07/4.41
% 13.07/4.41 %Foreground operators:
% 13.07/4.41 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 13.07/4.41 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 13.07/4.41 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 13.07/4.41 tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 13.07/4.41 tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 13.07/4.41 tff(uri_rdf_type, type, uri_rdf_type: $i).
% 13.07/4.41 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i).
% 13.07/4.41 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 13.07/4.41 tff(literal_typed, type, literal_typed: ($i * $i) > $i).
% 13.07/4.41 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 13.07/4.41 tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 13.07/4.41 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 13.07/4.41 tff(uri_rdf_List, type, uri_rdf_List: $i).
% 13.07/4.41 tff(uri_rdf_first, type, uri_rdf_first: $i).
% 13.07/4.41 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 13.07/4.41 tff(uri_ex_Person, type, uri_ex_Person: $i).
% 13.07/4.41 tff(uri_ex_bob, type, uri_ex_bob: $i).
% 13.07/4.41 tff(uri_rdf__3, type, uri_rdf__3: $i).
% 13.07/4.41 tff(icext, type, icext: ($i * $i) > $o).
% 13.07/4.41 tff(uri_rdf_value, type, uri_rdf_value: $i).
% 13.07/4.41 tff(ip, type, ip: $i > $o).
% 13.07/4.41 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 13.07/4.41 tff(uri_ex_hasAncestor, type, uri_ex_hasAncestor: $i).
% 13.07/4.41 tff(uri_rdf__1, type, uri_rdf__1: $i).
% 13.07/4.41 tff(uri_owl_TransitiveProperty, type, uri_owl_TransitiveProperty: $i).
% 13.07/4.41 tff(lv, type, lv: $i > $o).
% 13.07/4.41 tff(ir, type, ir: $i > $o).
% 13.07/4.41 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i).
% 13.07/4.41 tff(uri_ex_alice, type, uri_ex_alice: $i).
% 13.07/4.41 tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 13.07/4.41 tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 13.07/4.41 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 13.07/4.41 tff(ic, type, ic: $i > $o).
% 13.07/4.41 tff('#skF_1', type, '#skF_1': $i).
% 13.07/4.41 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 13.07/4.41 tff(uri_rdf_object, type, uri_rdf_object: $i).
% 13.07/4.41 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 13.07/4.41 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 13.07/4.41 tff(iext, type, iext: ($i * $i * $i) > $o).
% 13.07/4.41 tff(dat_str_1, type, dat_str_1: $i).
% 13.07/4.41 tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 13.07/4.41 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 13.07/4.41 tff(uri_rdf__2, type, uri_rdf__2: $i).
% 13.07/4.41 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 13.07/4.41 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 13.07/4.41 tff(uri_xsd_nonNegativeInteger, type, uri_xsd_nonNegativeInteger: $i).
% 13.07/4.41 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 13.07/4.41 tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 13.07/4.41 tff(uri_owl_minCardinality, type, uri_owl_minCardinality: $i).
% 13.07/4.41 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 13.07/4.41 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 13.07/4.41
% 13.07/4.41 %Saturated clause set:
% 13.07/4.41 tff(c_10266, plain, (![P_86]: (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, P_86) | ~iext(uri_rdfs_subPropertyOf, P_86, uri_rdfs_isDefinedBy)))).
% 13.07/4.41 tff(c_10257, plain, (![C_89]: (~iext(uri_rdfs_range, uri_owl_minCardinality, C_89) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_Bag)))).
% 13.07/4.41 tff(c_10248, plain, (![C_89]: (~iext(uri_rdfs_range, uri_owl_minCardinality, C_89) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_XMLLiteral)))).
% 13.07/4.41 tff(c_10239, plain, (![C_89]: (~iext(uri_rdfs_range, uri_owl_minCardinality, C_89) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_Alt)))).
% 13.07/4.41 tff(c_10238, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_minCardinality))).
% 13.07/4.41 tff(c_10220, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.07/4.41 tff(c_8056, plain, (![C_28, C_374]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_374) | ~iext(uri_rdfs_subClassOf, C_374, uri_ex_Person)))).
% 13.07/4.41 tff(c_10119, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_isDefinedBy))).
% 13.07/4.41 tff(c_5545, plain, (![Q_32, Q_335]: (iext(Q_32, '#skF_1', literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) | ~iext(uri_rdfs_subPropertyOf, Q_335, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, Q_335)))).
% 13.07/4.41 tff(c_8394, plain, (![Q_32, C_375]: (iext(Q_32, C_375, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_375, uri_rdfs_ContainerMembershipProperty)))).
% 13.07/4.41 tff(c_8393, plain, (![C_28, C_375]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_375) | ~iext(uri_rdfs_subClassOf, C_375, uri_rdfs_ContainerMembershipProperty)))).
% 13.07/4.41 tff(c_7217, plain, (![Q_32, C_361]: (iext(Q_32, C_361, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_361, uri_rdf_Bag)))).
% 13.07/4.41 tff(c_7216, plain, (![C_28, C_361]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_361) | ~iext(uri_rdfs_subClassOf, C_361, uri_rdf_Bag)))).
% 13.07/4.41 tff(c_8057, plain, (![Q_32, C_374]: (iext(Q_32, C_374, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_374, uri_ex_Person)))).
% 13.07/4.41 tff(c_8761, plain, (![C_28, C_378]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_378) | ~iext(uri_rdfs_subClassOf, C_378, uri_rdfs_Datatype)))).
% 13.07/4.41 tff(c_9755, plain, (![D_11]: (~iext(uri_rdfs_range, uri_owl_minCardinality, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.07/4.41 tff(c_9754, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdf_Alt))).
% 13.07/4.41 tff(c_9753, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdf_Bag))).
% 13.07/4.41 tff(c_9752, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdfs_Seq))).
% 13.07/4.41 tff(c_9751, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_ex_Person))).
% 13.07/4.41 tff(c_9750, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdf_XMLLiteral))).
% 13.07/4.41 tff(c_5390, plain, (![D_24, C_320]: (icext(D_24, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) | ~iext(uri_rdfs_subClassOf, C_320, D_24) | ~iext(uri_rdfs_range, uri_owl_minCardinality, C_320)))).
% 13.07/4.41 tff(c_8762, plain, (![Q_32, C_378]: (iext(Q_32, C_378, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_378, uri_rdfs_Datatype)))).
% 13.07/4.41 tff(c_7648, plain, (![Q_32, C_366]: (iext(Q_32, C_366, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_366, uri_rdf_Alt)))).
% 13.07/4.41 tff(c_7647, plain, (![C_28, C_366]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_366) | ~iext(uri_rdfs_subClassOf, C_366, uri_rdf_Alt)))).
% 13.07/4.41 tff(c_9418, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_comment))).
% 13.07/4.42 tff(c_6881, plain, (![C_28, C_360]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_360) | ~iext(uri_rdfs_subClassOf, C_360, uri_rdf_XMLLiteral)))).
% 13.07/4.42 tff(c_9417, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_label))).
% 13.07/4.42 tff(c_5546, plain, (![C_20, Q_335]: (icext(C_20, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) | ~iext(uri_rdfs_range, Q_335, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, Q_335)))).
% 13.07/4.42 tff(c_6882, plain, (![Q_32, C_360]: (iext(Q_32, C_360, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_360, uri_rdf_XMLLiteral)))).
% 13.07/4.42 tff(c_9332, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 13.07/4.42 tff(c_3883, plain, (![P_38, P_248]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_248) | ~iext(uri_rdfs_subPropertyOf, P_248, uri_rdfs_isDefinedBy)))).
% 13.07/4.42 tff(c_9313, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 13.07/4.42 tff(c_5270, plain, (![C_28, C_308]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_308) | ~iext(uri_rdfs_subClassOf, C_308, uri_rdf_XMLLiteral)))).
% 13.07/4.42 tff(c_3009, plain, (![Q_32, C_211]: (iext(Q_32, C_211, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_211, uri_rdf_Bag)))).
% 13.07/4.42 tff(c_4528, plain, (![Q_32, C_275]: (iext(Q_32, C_275, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_275, uri_rdf_Alt)))).
% 13.07/4.42 tff(c_3008, plain, (![C_28, C_211]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_211) | ~iext(uri_rdfs_subClassOf, C_211, uri_rdf_Bag)))).
% 13.07/4.42 tff(c_4527, plain, (![C_28, C_275]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_275) | ~iext(uri_rdfs_subClassOf, C_275, uri_rdf_Alt)))).
% 13.07/4.42 tff(c_5271, plain, (![Q_32, C_308]: (iext(Q_32, C_308, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_308, uri_rdf_XMLLiteral)))).
% 13.07/4.42 tff(c_3884, plain, (![Q_32, P_248]: (iext(Q_32, P_248, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_248, uri_rdfs_isDefinedBy)))).
% 13.07/4.42 tff(c_6289, plain, (![C_28, D_348]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_348) | ~icext(uri_rdfs_Datatype, D_348)))).
% 13.07/4.42 tff(c_6290, plain, (![Q_32, D_348]: (iext(Q_32, D_348, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_348)))).
% 13.07/4.42 tff(c_8865, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_object))).
% 13.07/4.42 tff(c_8864, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_rest))).
% 13.07/4.42 tff(c_8863, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_subject))).
% 13.07/4.42 tff(c_8862, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_predicate))).
% 13.07/4.42 tff(c_8861, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_domain))).
% 13.07/4.42 tff(c_8860, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_range))).
% 13.07/4.42 tff(c_8859, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_first))).
% 13.07/4.42 tff(c_5547, plain, (![C_13, Q_335]: (icext(C_13, '#skF_1') | ~iext(uri_rdfs_domain, Q_335, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, Q_335)))).
% 13.07/4.42 tff(c_8785, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 13.07/4.42 tff(c_5955, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_5907, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 13.07/4.42 tff(c_5856, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_8417, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 13.07/4.42 tff(c_5718, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_5954, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 13.07/4.42 tff(c_5759, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_ex_Person)))).
% 13.07/4.42 tff(c_5823, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 13.07/4.42 tff(c_5824, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_7704, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 13.07/4.42 tff(c_1512, plain, (![P_86, P_10]: (iext(uri_rdfs_subPropertyOf, P_86, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_86, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.07/4.42 tff(c_7686, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 13.07/4.42 tff(c_1429, plain, (![Q_82, P_10]: (iext(Q_82, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_82) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.07/4.42 tff(c_5908, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_5663, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_Alt)))).
% 13.07/4.42 tff(c_1428, plain, (![Q_82, D_11]: (iext(Q_82, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.07/4.42 tff(c_7303, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 13.07/4.42 tff(c_7226, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, uri_rdfs_isDefinedBy))).
% 13.07/4.42 tff(c_1538, plain, (![C_89, D_11]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_89, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.07/4.42 tff(c_7225, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdfs_Datatype))).
% 13.07/4.42 tff(c_5855, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_Bag)))).
% 13.07/4.42 tff(c_6890, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdfs_ContainerMembershipProperty))).
% 13.07/4.42 tff(c_5660, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_XMLLiteral)))).
% 13.07/4.42 tff(c_1430, plain, (![Q_82, X_7, C_8]: (iext(Q_82, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82) | ~icext(C_8, X_7)))).
% 13.07/4.42 tff(c_5760, plain, (![Q_32]: (iext(Q_32, uri_ex_Person, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_6422, plain, (![C_78]: (icext(uri_rdfs_Class, C_78) | ~iext(uri_rdfs_range, uri_owl_minCardinality, C_78)))).
% 13.07/4.42 tff(c_6316, plain, (![C_351, X_352]: (icext(uri_rdfs_Class, C_351) | ~icext(C_351, X_352)))).
% 13.07/4.42 tff(c_1204, plain, (![C_78, C_8, X_7]: (icext(C_78, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_78) | ~icext(C_8, X_7)))).
% 13.07/4.42 tff(c_5792, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.07/4.42 tff(c_5669, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.07/4.42 tff(c_5691, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_5694, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_1433, plain, (![Q_82, C_9]: (iext(Q_82, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82) | ~ic(C_9)))).
% 13.07/4.43 tff(c_5688, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_5685, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_5682, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_5679, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_5676, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 13.07/4.43 tff(c_1539, plain, (![C_89, C_9]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_89, C_9) | ~ic(C_9)))).
% 13.07/4.43 tff(c_5626, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdf_Property))).
% 13.07/4.43 tff(c_1435, plain, (![Q_82, C_27]: (iext(Q_82, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82) | ~ic(C_27)))).
% 13.07/4.43 tff(c_1431, plain, (![Q_82, P_37]: (iext(Q_82, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_82) | ~ip(P_37)))).
% 13.07/4.43 tff(c_5589, plain, (![C_78]: (icext(C_78, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_78)))).
% 13.07/4.43 tff(c_5583, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdf_type))).
% 13.07/4.43 tff(c_5561, plain, (![P_337]: (icext(uri_rdf_Property, P_337) | ~icext(uri_rdfs_ContainerMembershipProperty, P_337)))).
% 13.07/4.43 tff(c_5557, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_rdfs_isDefinedBy))).
% 13.07/4.43 tff(c_978, plain, (![C_74, P_10]: (icext(C_74, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_74) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.07/4.43 tff(c_5556, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_subClassOf))).
% 13.07/4.43 tff(c_5555, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_rdfs_subPropertyOf))).
% 13.07/4.43 tff(c_1434, plain, (![Q_82]: (iext(Q_82, '#skF_1', literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) | ~iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, Q_82)))).
% 13.07/4.43 tff(c_5496, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 13.07/4.43 tff(c_5484, plain, (![D_333]: (icext(uri_rdfs_Class, D_333) | ~icext(uri_rdfs_Datatype, D_333)))).
% 13.07/4.43 tff(c_5480, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 13.07/4.43 tff(c_977, plain, (![C_74, D_11]: (icext(C_74, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.07/4.43 tff(c_5479, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 13.07/4.43 tff(c_5478, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 13.07/4.43 tff(c_979, plain, (![C_74, X_7, C_8]: (icext(C_74, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74) | ~icext(C_8, X_7)))).
% 13.07/4.43 tff(c_5472, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_1432, plain, (![Q_82, P_6]: (iext(Q_82, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82) | ~ip(P_6)))).
% 13.07/4.43 tff(c_1647, plain, (![D_24, P_93]: (icext(D_24, P_93) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_93)))).
% 13.07/4.43 tff(c_5427, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdfs_Literal))).
% 13.07/4.43 tff(c_823, plain, (![D_71, X_16]: (icext(D_71, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_71) | ~ic(X_16)))).
% 13.07/4.43 tff(c_5397, plain, (~iext(uri_rdfs_range, uri_owl_minCardinality, uri_rdfs_Class))).
% 13.07/4.43 tff(c_1209, plain, (![C_78, C_27]: (icext(C_78, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78) | ~ic(C_27)))).
% 13.07/4.43 tff(c_1208, plain, (![C_78]: (icext(C_78, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) | ~iext(uri_rdfs_range, uri_owl_minCardinality, C_78)))).
% 13.07/4.43 tff(c_5363, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_5362, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_1205, plain, (![C_78, P_37]: (icext(C_78, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_78) | ~ip(P_37)))).
% 13.07/4.43 tff(c_5357, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_5327, plain, (~iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_822, plain, (![D_71, X_18]: (icext(D_71, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_71) | ~lv(X_18)))).
% 13.07/4.43 tff(c_5320, plain, (![C_78]: (icext(C_78, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.07/4.43 tff(c_980, plain, (![C_74, P_37]: (icext(C_74, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_74) | ~ip(P_37)))).
% 13.07/4.43 tff(c_5292, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_5291, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_982, plain, (![C_74, C_9]: (icext(C_74, C_9) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74) | ~ic(C_9)))).
% 13.07/4.43 tff(c_5286, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_5280, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_981, plain, (![C_74, P_6]: (icext(C_74, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74) | ~ip(P_6)))).
% 13.07/4.43 tff(c_5279, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 13.07/4.43 tff(c_1541, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_XMLLiteral)))).
% 13.07/4.43 tff(c_1467, plain, (![Q_82]: (iext(Q_82, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.43 tff(c_1496, plain, (![Q_82]: (iext(Q_82, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.43 tff(c_1452, plain, (![Q_82]: (iext(Q_82, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.43 tff(c_1546, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdfs_ContainerMembershipProperty)))).
% 13.07/4.43 tff(c_1446, plain, (![Q_82]: (iext(Q_82, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.43 tff(c_1444, plain, (![Q_82]: (iext(Q_82, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.43 tff(c_1440, plain, (![Q_82]: (iext(Q_82, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.43 tff(c_1447, plain, (![Q_82]: (iext(Q_82, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.43 tff(c_1484, plain, (![Q_82]: (iext(Q_82, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.43 tff(c_1490, plain, (![Q_82]: (iext(Q_82, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.43 tff(c_1498, plain, (![Q_82]: (iext(Q_82, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.43 tff(c_1439, plain, (![Q_82]: (iext(Q_82, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.43 tff(c_1497, plain, (![Q_82]: (iext(Q_82, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1542, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, '#skF_1') | ~iext(uri_rdfs_subClassOf, C_89, uri_ex_Person)))).
% 13.07/4.44 tff(c_1459, plain, (![Q_82]: (iext(Q_82, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1463, plain, (![Q_82]: (iext(Q_82, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1458, plain, (![Q_82]: (iext(Q_82, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_4771, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Alt))).
% 13.07/4.44 tff(c_1480, plain, (![Q_82]: (iext(Q_82, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1493, plain, (![Q_82]: (iext(Q_82, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1455, plain, (![Q_82]: (iext(Q_82, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1477, plain, (![Q_82]: (iext(Q_82, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1438, plain, (![Q_82]: (iext(Q_82, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1462, plain, (![Q_82]: (iext(Q_82, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1453, plain, (![Q_82]: (iext(Q_82, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1465, plain, (![Q_82]: (iext(Q_82, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_4635, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1454, plain, (![Q_82]: (iext(Q_82, uri_ex_Person, '#skF_1') | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1491, plain, (![Q_82]: (iext(Q_82, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_4619, plain, (~iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_rdf_Alt))).
% 13.07/4.44 tff(c_4618, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1451, plain, (![Q_82]: (iext(Q_82, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_4602, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_ex_hasAncestor))).
% 13.07/4.44 tff(c_4586, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1488, plain, (![Q_82]: (iext(Q_82, uri_ex_alice, uri_ex_bob) | ~iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, Q_82)))).
% 13.07/4.44 tff(c_4585, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1460, plain, (![Q_82]: (iext(Q_82, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_4569, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 13.07/4.44 tff(c_4553, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1495, plain, (![Q_82]: (iext(Q_82, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_4552, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Alt))).
% 13.07/4.44 tff(c_4551, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 13.07/4.44 tff(c_1450, plain, (![Q_82]: (iext(Q_82, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1543, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_Alt)))).
% 13.07/4.44 tff(c_1489, plain, (![Q_82]: (iext(Q_82, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1461, plain, (![Q_82]: (iext(Q_82, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1483, plain, (![Q_82]: (iext(Q_82, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1445, plain, (![Q_82]: (iext(Q_82, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1544, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Seq)))).
% 13.07/4.44 tff(c_1486, plain, (![Q_82]: (iext(Q_82, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1501, plain, (![Q_82]: (iext(Q_82, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1547, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Datatype)))).
% 13.07/4.44 tff(c_1436, plain, (![Q_82]: (iext(Q_82, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1466, plain, (![Q_82]: (iext(Q_82, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1492, plain, (![Q_82]: (iext(Q_82, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1479, plain, (![Q_82]: (iext(Q_82, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1464, plain, (![Q_82]: (iext(Q_82, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1468, plain, (![Q_82]: (iext(Q_82, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1478, plain, (![Q_82]: (iext(Q_82, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.07/4.44 tff(c_1443, plain, (![Q_82]: (iext(Q_82, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1475, plain, (![Q_82]: (iext(Q_82, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1457, plain, (![Q_82]: (iext(Q_82, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1487, plain, (![Q_82]: (iext(Q_82, uri_ex_hasAncestor, uri_owl_TransitiveProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1448, plain, (![Q_82]: (iext(Q_82, '#skF_1', uri_owl_Restriction) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1442, plain, (![Q_82]: (iext(Q_82, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_3953, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_onProperty))).
% 13.07/4.44 tff(c_1469, plain, (![Q_82]: (iext(Q_82, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1499, plain, (![Q_82]: (iext(Q_82, '#skF_1', uri_ex_hasAncestor) | ~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_82)))).
% 13.07/4.44 tff(c_1473, plain, (![Q_82]: (iext(Q_82, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_3922, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 13.07/4.44 tff(c_1500, plain, (![Q_82]: (iext(Q_82, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_82)))).
% 13.07/4.44 tff(c_1470, plain, (![Q_82]: (iext(Q_82, uri_ex_alice, uri_ex_Person) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_3816, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Bag))).
% 13.07/4.44 tff(c_1514, plain, (![P_86]: (iext(uri_rdfs_subPropertyOf, P_86, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_86, uri_rdfs_isDefinedBy)))).
% 13.07/4.44 tff(c_1474, plain, (![Q_82]: (iext(Q_82, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.44 tff(c_1441, plain, (![Q_82]: (iext(Q_82, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_2870, plain, (![D_24]: (icext(D_24, uri_ex_bob) | ~iext(uri_rdfs_subClassOf, '#skF_1', D_24)))).
% 13.07/4.44 tff(c_3768, plain, (~icext(uri_rdfs_Datatype, '#skF_1'))).
% 13.07/4.44 tff(c_2770, plain, (![D_24]: (icext(D_24, uri_ex_alice) | ~iext(uri_rdfs_subClassOf, '#skF_1', D_24)))).
% 13.07/4.44 tff(c_2003, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.44 tff(c_1757, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.44 tff(c_1437, plain, (![Q_82]: (iext(Q_82, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.07/4.44 tff(c_1891, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.44 tff(c_1776, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.44 tff(c_1985, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.44 tff(c_2026, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.44 tff(c_1808, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.44 tff(c_1738, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.44 tff(c_1916, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.45 tff(c_2267, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.45 tff(c_1851, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.45 tff(c_1456, plain, (![Q_82]: (iext(Q_82, uri_ex_bob, uri_ex_Person) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.07/4.45 tff(c_1927, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.45 tff(c_1727, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.07/4.45 tff(c_2145, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.07/4.45 tff(c_1819, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2119, plain, (![D_24]: (icext(D_24, uri_ex_Person) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2108, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_3295, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 13.39/4.45 tff(c_1476, plain, (![Q_82]: (iext(Q_82, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.39/4.45 tff(c_3283, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 13.39/4.45 tff(c_3282, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 13.39/4.45 tff(c_1864, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_1485, plain, (![Q_82]: (iext(Q_82, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.39/4.45 tff(c_3245, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 13.39/4.45 tff(c_2176, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2322, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_3194, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 13.39/4.45 tff(c_1481, plain, (![Q_82]: (iext(Q_82, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_82)))).
% 13.39/4.45 tff(c_3182, plain, (~iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_rdf_Bag))).
% 13.39/4.45 tff(c_3181, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 13.39/4.45 tff(c_2084, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1966, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1789, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1472, plain, (![Q_82]: (iext(Q_82, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.39/4.45 tff(c_3094, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Bag))).
% 13.39/4.45 tff(c_3093, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdf_Bag))).
% 13.39/4.45 tff(c_2341, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2372, plain, (![D_24]: (icext(D_24, uri_owl_TransitiveProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2189, plain, (![D_24]: (icext(D_24, uri_owl_Restriction) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_3017, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 13.39/4.45 tff(c_1545, plain, (![C_89]: (iext(uri_rdfs_subClassOf, C_89, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_89, uri_rdf_Bag)))).
% 13.39/4.45 tff(c_1557, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2867, plain, (icext('#skF_1', uri_ex_bob))).
% 13.39/4.45 tff(c_1586, plain, (![D_24]: (icext(D_24, uri_ex_bob) | ~iext(uri_rdfs_subClassOf, uri_ex_Person, D_24)))).
% 13.39/4.45 tff(c_1554, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2823, plain, (~icext(uri_rdfs_Datatype, uri_owl_TransitiveProperty))).
% 13.39/4.45 tff(c_1595, plain, (![D_24]: (icext(D_24, uri_ex_hasAncestor) | ~iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, D_24)))).
% 13.39/4.45 tff(c_1560, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2771, plain, (~icext(uri_rdfs_Datatype, uri_ex_Person))).
% 13.39/4.45 tff(c_1449, plain, (![Q_82]: (iext(Q_82, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.39/4.45 tff(c_2767, plain, (icext('#skF_1', uri_ex_alice))).
% 13.39/4.45 tff(c_1604, plain, (![D_24]: (icext(D_24, uri_ex_alice) | ~iext(uri_rdfs_subClassOf, uri_ex_Person, D_24)))).
% 13.39/4.45 tff(c_2743, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 13.39/4.45 tff(c_1598, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.39/4.45 tff(c_1607, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.39/4.45 tff(c_2692, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 13.39/4.45 tff(c_1482, plain, (![Q_82]: (iext(Q_82, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_82)))).
% 13.39/4.45 tff(c_2680, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 13.39/4.45 tff(c_1569, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1566, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2619, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 13.39/4.45 tff(c_1583, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1592, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 13.39/4.45 tff(c_1572, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_1494, plain, (![Q_82]: (iext(Q_82, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_82)))).
% 13.39/4.45 tff(c_2567, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 13.39/4.45 tff(c_1578, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.39/4.45 tff(c_2546, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.45 tff(c_1589, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.39/4.45 tff(c_1601, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2500, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 13.39/4.45 tff(c_1471, plain, (![Q_82]: (iext(Q_82, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_82)))).
% 13.39/4.45 tff(c_1563, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.39/4.45 tff(c_2468, plain, (~icext(uri_rdfs_Datatype, uri_owl_Restriction))).
% 13.39/4.45 tff(c_1551, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_24)))).
% 13.39/4.45 tff(c_2447, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 13.39/4.45 tff(c_1610, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 13.39/4.45 tff(c_1259, plain, (![C_78]: (icext(C_78, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_78)))).
% 13.39/4.45 tff(c_1003, plain, (![C_74]: (icext(C_74, uri_ex_Person) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.45 tff(c_1008, plain, (![C_74]: (icext(C_74, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.45 tff(c_1020, plain, (![C_74]: (icext(C_74, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_74)))).
% 13.39/4.45 tff(c_1042, plain, (![C_74]: (icext(C_74, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.45 tff(c_1267, plain, (![C_78]: (icext(C_78, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.45 tff(c_1022, plain, (![C_74]: (icext(C_74, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.45 tff(c_1025, plain, (![C_74]: (icext(C_74, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.45 tff(c_2373, plain, (ic(uri_owl_TransitiveProperty))).
% 13.39/4.45 tff(c_2366, plain, (icext(uri_rdfs_Class, uri_owl_TransitiveProperty))).
% 13.39/4.45 tff(c_1261, plain, (![C_78]: (icext(C_78, uri_owl_TransitiveProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.45 tff(c_1046, plain, (![C_74]: (icext(C_74, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.45 tff(c_1015, plain, (![C_74]: (icext(C_74, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.45 tff(c_1016, plain, (![C_74]: (icext(C_74, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.45 tff(c_2335, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 13.39/4.45 tff(c_1229, plain, (![C_78]: (icext(C_78, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.39/4.45 tff(c_1043, plain, (![C_74]: (icext(C_74, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.45 tff(c_2316, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 13.39/4.45 tff(c_1018, plain, (![C_74]: (icext(C_74, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.45 tff(c_1040, plain, (![C_74]: (icext(C_74, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.45 tff(c_1036, plain, (![C_74]: (icext(C_74, uri_ex_hasAncestor) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.45 tff(c_993, plain, (![C_74]: (icext(C_74, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.45 tff(c_1038, plain, (![C_74]: (icext(C_74, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.45 tff(c_1220, plain, (![C_78]: (icext(C_78, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.39/4.46 tff(c_997, plain, (![C_74]: (icext(C_74, '#skF_1') | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1248, plain, (![C_78]: (icext(C_78, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_2261, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 13.39/4.46 tff(c_1004, plain, (![C_74]: (icext(C_74, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.46 tff(c_1005, plain, (![C_74]: (icext(C_74, uri_ex_bob) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_992, plain, (![C_74]: (icext(C_74, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1002, plain, (![C_74]: (icext(C_74, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1027, plain, (![C_74]: (icext(C_74, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1010, plain, (![C_74]: (icext(C_74, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1274, plain, (![C_78]: (icext(C_78, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.39/4.46 tff(c_1000, plain, (![C_74]: (icext(C_74, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_2214, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 13.39/4.46 tff(c_824, plain, (![D_71, X_17]: (icext(D_71, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_71)))).
% 13.39/4.46 tff(c_1029, plain, (![C_74]: (icext(C_74, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.46 tff(c_2190, plain, (ic(uri_owl_Restriction))).
% 13.39/4.46 tff(c_2183, plain, (icext(uri_rdfs_Class, uri_owl_Restriction))).
% 13.39/4.46 tff(c_1222, plain, (![C_78]: (icext(C_78, uri_owl_Restriction) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_2170, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 13.39/4.46 tff(c_1275, plain, (![C_78]: (icext(C_78, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_78)))).
% 13.39/4.46 tff(c_987, plain, (![C_74]: (icext(C_74, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1019, plain, (![C_74]: (icext(C_74, uri_ex_alice) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1245, plain, (![C_78]: (icext(C_78, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_78)))).
% 13.39/4.46 tff(c_2139, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 13.39/4.46 tff(c_1013, plain, (![C_74]: (icext(C_74, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.46 tff(c_1037, plain, (![C_74]: (icext(C_74, uri_ex_alice) | ~iext(uri_rdfs_domain, uri_ex_hasAncestor, C_74)))).
% 13.39/4.46 tff(c_1219, plain, (![C_78]: (icext(C_78, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_78)))).
% 13.39/4.46 tff(c_1006, plain, (![C_74]: (icext(C_74, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_2113, plain, (icext(uri_rdfs_Class, uri_ex_Person))).
% 13.39/4.46 tff(c_1244, plain, (![C_78]: (icext(C_78, uri_ex_Person) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_2107, plain, (ip(uri_rdfs_label))).
% 13.39/4.46 tff(c_2101, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 13.39/4.46 tff(c_990, plain, (![C_74]: (icext(C_74, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_985, plain, (![C_74]: (icext(C_74, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1254, plain, (![C_78]: (icext(C_78, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.39/4.46 tff(c_2076, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 13.39/4.46 tff(c_1028, plain, (![C_74]: (icext(C_74, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1041, plain, (![C_74]: (icext(C_74, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_983, plain, (![C_74]: (icext(C_74, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_minCardinality, C_74)))).
% 13.39/4.46 tff(c_1050, plain, (![C_74]: (icext(C_74, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1031, plain, (![C_74]: (icext(C_74, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1047, plain, (![C_74]: (icext(C_74, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1026, plain, (![C_74]: (icext(C_74, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1262, plain, (![C_78]: (icext(C_78, uri_ex_bob) | ~iext(uri_rdfs_range, uri_ex_hasAncestor, C_78)))).
% 13.39/4.46 tff(c_1030, plain, (![C_74]: (icext(C_74, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1009, plain, (![C_74]: (icext(C_74, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_2027, plain, (ic(uri_rdfs_Statement))).
% 13.39/4.46 tff(c_2020, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 13.39/4.46 tff(c_1237, plain, (![C_78]: (icext(C_78, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_78)))).
% 13.39/4.46 tff(c_1014, plain, (![C_74]: (icext(C_74, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1032, plain, (![C_74]: (icext(C_74, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_2002, plain, (ip(uri_rdfs_comment))).
% 13.39/4.46 tff(c_1996, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 13.39/4.46 tff(c_1045, plain, (![C_74]: (icext(C_74, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1011, plain, (![C_74]: (icext(C_74, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1977, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 13.39/4.46 tff(c_1039, plain, (![C_74]: (icext(C_74, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1212, plain, (![C_78]: (icext(C_78, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_78)))).
% 13.39/4.46 tff(c_1958, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 13.39/4.46 tff(c_994, plain, (![C_74]: (icext(C_74, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1213, plain, (![C_78]: (icext(C_78, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_78)))).
% 13.39/4.46 tff(c_1044, plain, (![C_74]: (icext(C_74, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_986, plain, (![C_74]: (icext(C_74, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_991, plain, (![C_74]: (icext(C_74, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1921, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 13.39/4.46 tff(c_995, plain, (![C_74]: (icext(C_74, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.46 tff(c_1908, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 13.39/4.46 tff(c_999, plain, (![C_74]: (icext(C_74, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1251, plain, (![C_78]: (icext(C_78, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_78)))).
% 13.39/4.46 tff(c_989, plain, (![C_74]: (icext(C_74, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1883, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 13.39/4.46 tff(c_1034, plain, (![C_74]: (icext(C_74, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1024, plain, (![C_74]: (icext(C_74, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_996, plain, (![C_74]: (icext(C_74, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1858, plain, (icext(uri_rdfs_Class, '#skF_1'))).
% 13.39/4.46 tff(c_1228, plain, (![C_78]: (icext(C_78, '#skF_1') | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_78)))).
% 13.39/4.46 tff(c_1839, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 13.39/4.46 tff(c_988, plain, (![C_74]: (icext(C_74, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1049, plain, (![C_74]: (icext(C_74, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_74)))).
% 13.39/4.46 tff(c_1273, plain, (![C_78]: (icext(C_78, uri_ex_hasAncestor) | ~iext(uri_rdfs_range, uri_owl_onProperty, C_78)))).
% 13.39/4.46 tff(c_1001, plain, (![C_74]: (icext(C_74, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1236, plain, (![C_78]: (icext(C_78, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_78)))).
% 13.39/4.46 tff(c_1813, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 13.39/4.46 tff(c_1216, plain, (![C_78]: (icext(C_78, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_78)))).
% 13.39/4.46 tff(c_1794, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 13.39/4.46 tff(c_1023, plain, (![C_74]: (icext(C_74, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_74)))).
% 13.39/4.46 tff(c_1033, plain, (![C_74]: (icext(C_74, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1788, plain, (ip(uri_rdf_predicate))).
% 13.39/4.46 tff(c_1782, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 13.39/4.46 tff(c_1012, plain, (![C_74]: (icext(C_74, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1777, plain, (ic(uri_rdf_List))).
% 13.39/4.46 tff(c_1770, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 13.39/4.46 tff(c_1218, plain, (![C_78]: (icext(C_78, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_1021, plain, (![C_74]: (icext(C_74, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_74)))).
% 13.39/4.46 tff(c_1745, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 13.39/4.46 tff(c_1221, plain, (![C_78]: (icext(C_78, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_1270, plain, (![C_78]: (icext(C_78, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_78)))).
% 13.39/4.46 tff(c_1732, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.46 tff(c_1242, plain, (![C_78]: (icext(C_78, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_78)))).
% 13.39/4.46 tff(c_1719, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 13.39/4.46 tff(c_1035, plain, (![C_74]: (icext(C_74, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_74)))).
% 13.39/4.46 tff(c_1048, plain, (![C_74]: (icext(C_74, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_onProperty, C_74)))).
% 13.39/4.46 tff(c_686, plain, (![X_65]: (ip(X_65) | ~icext(uri_rdf_Property, X_65)))).
% 13.39/4.46 tff(c_790, plain, (![P_69]: (ip(P_69) | ~icext(uri_rdfs_ContainerMembershipProperty, P_69)))).
% 13.39/4.46 tff(c_756, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 13.39/4.46 tff(c_807, plain, (![D_70]: (ic(D_70) | ~icext(uri_rdfs_Datatype, D_70)))).
% 13.39/4.46 tff(c_1637, plain, (ip(uri_rdfs_member))).
% 13.39/4.46 tff(c_1631, plain, (ic(uri_rdfs_Resource))).
% 13.39/4.46 tff(c_768, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 13.39/4.46 tff(c_765, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 13.39/4.46 tff(c_766, plain, (icext(uri_ex_Person, uri_ex_alice))).
% 13.39/4.46 tff(c_774, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 13.39/4.46 tff(c_770, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 13.39/4.46 tff(c_771, plain, (icext(uri_owl_TransitiveProperty, uri_ex_hasAncestor))).
% 13.39/4.46 tff(c_758, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 13.39/4.46 tff(c_763, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 13.39/4.46 tff(c_762, plain, (icext(uri_ex_Person, uri_ex_bob))).
% 13.39/4.46 tff(c_761, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 13.39/4.46 tff(c_773, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 13.39/4.46 tff(c_769, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 13.39/4.46 tff(c_764, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 13.39/4.46 tff(c_772, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 13.39/4.46 tff(c_767, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 13.39/4.46 tff(c_757, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 13.39/4.46 tff(c_759, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 13.39/4.46 tff(c_775, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 13.39/4.46 tff(c_760, plain, (icext(uri_owl_Restriction, '#skF_1'))).
% 13.39/4.47 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)))).
% 13.39/4.47 tff(c_669, plain, (ic(uri_ex_Person))).
% 13.39/4.47 tff(c_286, plain, (ip(uri_rdf_object))).
% 13.39/4.47 tff(c_668, plain, (ic(uri_rdf_XMLLiteral))).
% 13.39/4.47 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)))).
% 13.39/4.47 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)))).
% 13.39/4.47 tff(c_672, plain, (ic(uri_rdf_Bag))).
% 13.39/4.47 tff(c_670, plain, (ic(uri_rdf_Alt))).
% 13.39/4.47 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)))).
% 13.39/4.47 tff(c_496, plain, (ip(uri_owl_minCardinality))).
% 13.39/4.47 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)))).
% 13.39/4.47 tff(c_283, plain, (ip(uri_rdf_value))).
% 13.39/4.47 tff(c_282, plain, (ip(uri_rdf__2))).
% 13.39/4.47 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)))).
% 13.39/4.47 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.39/4.47 tff(c_284, plain, (ip(uri_rdf_subject))).
% 13.39/4.47 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.39/4.47 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 13.39/4.47 tff(c_671, plain, (ic(uri_rdfs_Seq))).
% 13.39/4.47 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 13.39/4.47 tff(c_673, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.47 tff(c_674, plain, (ic(uri_rdfs_Datatype))).
% 13.39/4.47 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 13.39/4.47 tff(c_633, plain, (ip(uri_rdfs_seeAlso))).
% 13.39/4.47 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 13.39/4.47 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 13.39/4.47 tff(c_565, plain, (ip(uri_ex_hasAncestor))).
% 13.39/4.47 tff(c_609, plain, (ip(uri_rdfs_isDefinedBy))).
% 13.39/4.47 tff(c_543, plain, (ip(uri_rdfs_subPropertyOf))).
% 13.39/4.47 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 13.39/4.47 tff(c_570, plain, (ip(uri_rdfs_domain))).
% 13.39/4.47 tff(c_287, plain, (ip(uri_rdf_rest))).
% 13.39/4.47 tff(c_533, plain, (ip(uri_rdfs_subClassOf))).
% 13.39/4.47 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 13.39/4.47 tff(c_281, plain, (ip(uri_rdf__3))).
% 13.39/4.47 tff(c_580, plain, (ip(uri_owl_onProperty))).
% 13.39/4.47 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 13.39/4.47 tff(c_288, plain, (ip(uri_rdf_first))).
% 13.39/4.47 tff(c_582, plain, (ip(uri_rdfs_range))).
% 13.39/4.47 tff(c_280, plain, (ip(uri_rdf__1))).
% 13.39/4.47 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 13.39/4.47 tff(c_285, plain, (ip(uri_rdf_type))).
% 13.39/4.47 tff(c_246, plain, (ic('#skF_1'))).
% 13.39/4.47 tff(c_249, plain, (ic(uri_rdfs_Container))).
% 13.39/4.47 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 13.39/4.47 tff(c_250, plain, (ic(uri_rdf_Property))).
% 13.39/4.47 tff(c_251, plain, (ic(uri_rdfs_Class))).
% 13.39/4.47 tff(c_245, plain, (ic(uri_rdfs_Literal))).
% 13.39/4.47 tff(c_188, plain, (iext(uri_owl_minCardinality, '#skF_1', literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)))).
% 13.39/4.47 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 13.39/4.47 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 13.39/4.47 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 13.39/4.47 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 13.39/4.47 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 13.39/4.47 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 13.39/4.47 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 13.39/4.47 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 13.39/4.47 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 13.39/4.47 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 13.39/4.47 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 13.39/4.47 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 13.39/4.47 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 13.39/4.47 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 13.39/4.47 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 13.39/4.47 tff(c_192, plain, (iext(uri_rdf_type, '#skF_1', uri_owl_Restriction))).
% 13.39/4.47 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 13.39/4.47 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 13.39/4.47 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 13.39/4.47 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 13.39/4.47 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_194, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, '#skF_1'))).
% 13.39/4.47 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 13.39/4.47 tff(c_184, plain, (iext(uri_rdf_type, uri_ex_bob, uri_ex_Person))).
% 13.39/4.47 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 13.39/4.47 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.47 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 13.39/4.47 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 13.39/4.47 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 13.39/4.47 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.47 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 13.39/4.47 tff(c_186, plain, (iext(uri_rdf_type, uri_ex_alice, uri_ex_Person))).
% 13.39/4.47 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 13.39/4.47 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 13.39/4.47 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 13.39/4.47 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 13.39/4.47 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 13.39/4.47 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 13.39/4.47 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 13.39/4.47 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 13.39/4.47 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 13.39/4.47 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 13.39/4.47 tff(c_196, plain, (iext(uri_rdf_type, uri_ex_hasAncestor, uri_owl_TransitiveProperty))).
% 13.39/4.47 tff(c_182, plain, (iext(uri_ex_hasAncestor, uri_ex_alice, uri_ex_bob))).
% 13.39/4.47 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 13.39/4.47 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 13.39/4.47 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 13.39/4.47 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_180, plain, (![BNODE_x_41]: (~iext(uri_ex_hasAncestor, uri_ex_alice, BNODE_x_41) | ~iext(uri_ex_hasAncestor, uri_ex_bob, BNODE_x_41)))).
% 13.39/4.47 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 13.39/4.47 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 13.39/4.47 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 13.39/4.47 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 13.39/4.47 tff(c_190, plain, (iext(uri_owl_onProperty, '#skF_1', uri_ex_hasAncestor))).
% 13.39/4.47 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 13.39/4.47 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 13.39/4.47 tff(c_202, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 13.39/4.47 tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 13.39/4.47 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.39/4.47
%------------------------------------------------------------------------------