%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWB012+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/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 09:15:49 PM UTC 2025
% Result : CounterSatisfiable 11.96s 4.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB012+4 : TPTP v9.0.0. Released v5.2.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n018.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Apr 9 00:55:47 EDT 2025
% 0.13/0.34 % CPUTime :
% 11.96/4.06
% 11.96/4.06 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.96/4.06
% 11.96/4.06 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.96/4.07 %$ iext > icext > lv > ir > ip > ic > #nlpp > literal_plain > 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_intersectionOf > uri_owl_hasValue > uri_owl_Restriction > uri_owl_FunctionalProperty > uri_owl_DatatypeProperty > uri_owl_Class > uri_foaf_Person > uri_ex_name > uri_ex_alice > uri_ex_PersonAttribute > dat_str_alice > #skF_2 > #skF_3 > #skF_1 > #skF_4
% 11.96/4.07
% 11.96/4.07 %Foreground sorts:
% 11.96/4.07
% 11.96/4.07
% 11.96/4.07 %Background operators:
% 11.96/4.07
% 11.96/4.07
% 11.96/4.07 %Foreground operators:
% 11.96/4.07 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 11.96/4.07 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 11.96/4.07 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 11.96/4.07 tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 11.96/4.07 tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 11.96/4.07 tff(uri_rdf_type, type, uri_rdf_type: $i).
% 11.96/4.07 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i).
% 11.96/4.07 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 11.96/4.07 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 11.96/4.07 tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 11.96/4.07 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 11.96/4.07 tff(uri_rdf_List, type, uri_rdf_List: $i).
% 11.96/4.07 tff(uri_rdf_first, type, uri_rdf_first: $i).
% 11.96/4.07 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 11.96/4.07 tff(uri_owl_intersectionOf, type, uri_owl_intersectionOf: $i).
% 11.96/4.07 tff(uri_owl_hasValue, type, uri_owl_hasValue: $i).
% 11.96/4.07 tff(uri_rdf__3, type, uri_rdf__3: $i).
% 11.96/4.07 tff(icext, type, icext: ($i * $i) > $o).
% 11.96/4.07 tff(uri_rdf_value, type, uri_rdf_value: $i).
% 11.96/4.07 tff(uri_owl_FunctionalProperty, type, uri_owl_FunctionalProperty: $i).
% 11.96/4.07 tff(ip, type, ip: $i > $o).
% 11.96/4.07 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 11.96/4.07 tff(uri_rdf__1, type, uri_rdf__1: $i).
% 11.96/4.07 tff(uri_foaf_Person, type, uri_foaf_Person: $i).
% 11.96/4.07 tff(lv, type, lv: $i > $o).
% 11.96/4.07 tff(uri_ex_PersonAttribute, type, uri_ex_PersonAttribute: $i).
% 11.96/4.07 tff(ir, type, ir: $i > $o).
% 11.96/4.07 tff(dat_str_alice, type, dat_str_alice: $i).
% 11.96/4.07 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i).
% 11.96/4.07 tff(uri_ex_alice, type, uri_ex_alice: $i).
% 11.96/4.07 tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 11.96/4.07 tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 11.96/4.07 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 11.96/4.07 tff(ic, type, ic: $i > $o).
% 11.96/4.07 tff('#skF_2', type, '#skF_2': $i).
% 11.96/4.07 tff('#skF_3', type, '#skF_3': $i).
% 11.96/4.07 tff('#skF_1', type, '#skF_1': $i).
% 11.96/4.07 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 11.96/4.07 tff(uri_rdf_object, type, uri_rdf_object: $i).
% 11.96/4.07 tff(uri_ex_name, type, uri_ex_name: $i).
% 11.96/4.07 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 11.96/4.07 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 11.96/4.07 tff(uri_owl_Class, type, uri_owl_Class: $i).
% 11.96/4.07 tff(iext, type, iext: ($i * $i * $i) > $o).
% 11.96/4.07 tff(uri_owl_DatatypeProperty, type, uri_owl_DatatypeProperty: $i).
% 11.96/4.07 tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 11.96/4.07 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 11.96/4.07 tff(uri_rdf__2, type, uri_rdf__2: $i).
% 11.96/4.07 tff('#skF_4', type, '#skF_4': $i).
% 11.96/4.07 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 11.96/4.07 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 11.96/4.07 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 11.96/4.07 tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 11.96/4.07 tff(literal_plain, type, literal_plain: $i > $i).
% 11.96/4.07 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 11.96/4.07 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 11.96/4.07
% 11.96/4.07 %Saturated clause set:
% 11.96/4.07 tff(c_9725, plain, (![P_87]: (~iext(uri_rdfs_subPropertyOf, uri_ex_name, P_87) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))).
% 11.96/4.07 tff(c_9724, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_ex_name))).
% 11.96/4.07 tff(c_9706, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_ex_name, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 11.96/4.07 tff(c_9705, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_isDefinedBy))).
% 11.96/4.07 tff(c_5532, plain, (![Q_32, Q_328]: (iext(Q_32, uri_ex_alice, literal_plain(dat_str_alice)) | ~iext(uri_rdfs_subPropertyOf, Q_328, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_ex_name, Q_328)))).
% 11.96/4.07 tff(c_7003, 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)))).
% 11.96/4.07 tff(c_8087, plain, (![Q_32, C_384]: (iext(Q_32, C_384, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_384, uri_rdfs_ContainerMembershipProperty)))).
% 11.96/4.07 tff(c_6233, plain, (![C_28, C_357]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_357) | ~iext(uri_rdfs_subClassOf, C_357, uri_rdf_Bag)))).
% 11.96/4.07 tff(c_8086, plain, (![C_28, C_384]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_384) | ~iext(uri_rdfs_subClassOf, C_384, uri_rdfs_ContainerMembershipProperty)))).
% 11.96/4.07 tff(c_7002, 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)))).
% 11.96/4.07 tff(c_8441, plain, (![Q_32, C_387]: (iext(Q_32, C_387, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_387, uri_rdfs_Datatype)))).
% 11.96/4.07 tff(c_6234, plain, (![Q_32, C_357]: (iext(Q_32, C_357, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_357, uri_rdf_Bag)))).
% 11.96/4.07 tff(c_8440, plain, (![C_28, C_387]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_387) | ~iext(uri_rdfs_subClassOf, C_387, uri_rdfs_Datatype)))).
% 11.96/4.07 tff(c_7571, plain, (![Q_32, C_370]: (iext(Q_32, C_370, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_370, uri_rdf_Alt)))).
% 11.96/4.07 tff(c_9248, plain, (![C_84]: (~iext(uri_rdfs_range, uri_ex_name, C_84) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_XMLLiteral)))).
% 11.96/4.08 tff(c_9239, plain, (![C_84]: (~iext(uri_rdfs_range, uri_ex_name, C_84) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Bag)))).
% 11.96/4.08 tff(c_9141, plain, (![C_84]: (~iext(uri_rdfs_range, uri_ex_name, C_84) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Alt)))).
% 11.96/4.08 tff(c_7570, plain, (![C_28, C_370]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_370) | ~iext(uri_rdfs_subClassOf, C_370, uri_rdf_Alt)))).
% 11.96/4.08 tff(c_5084, plain, (![Q_32, C_316]: (iext(Q_32, C_316, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_316, uri_rdf_Alt)))).
% 11.96/4.08 tff(c_5083, plain, (![C_28, C_316]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_316) | ~iext(uri_rdfs_subClassOf, C_316, uri_rdf_Alt)))).
% 12.11/4.08 tff(c_9042, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 12.11/4.08 tff(c_4322, plain, (![C_28, C_273]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_273) | ~iext(uri_rdfs_subClassOf, C_273, uri_rdf_XMLLiteral)))).
% 12.11/4.08 tff(c_4323, plain, (![Q_32, C_273]: (iext(Q_32, C_273, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_273, uri_rdf_XMLLiteral)))).
% 12.11/4.08 tff(c_8946, plain, (![D_11]: (~iext(uri_rdfs_range, uri_ex_name, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.08 tff(c_4049, plain, (![Q_32, C_271]: (iext(Q_32, C_271, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_271, uri_rdf_Bag)))).
% 12.11/4.08 tff(c_8930, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 12.11/4.08 tff(c_8929, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdfs_Seq))).
% 12.11/4.08 tff(c_8928, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdf_Alt))).
% 12.11/4.08 tff(c_8927, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdf_XMLLiteral))).
% 12.11/4.08 tff(c_8908, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdf_Bag))).
% 12.11/4.08 tff(c_5413, plain, (![P_38, P_319]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_319) | ~iext(uri_rdfs_subPropertyOf, P_319, uri_rdfs_isDefinedBy)))).
% 12.11/4.08 tff(c_4647, plain, (![D_24, C_299]: (icext(D_24, literal_plain(dat_str_alice)) | ~iext(uri_rdfs_subClassOf, C_299, D_24) | ~iext(uri_rdfs_range, uri_ex_name, C_299)))).
% 12.11/4.08 tff(c_8817, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_label))).
% 12.11/4.08 tff(c_8816, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_comment))).
% 12.11/4.08 tff(c_5534, plain, (![C_20, Q_328]: (icext(C_20, literal_plain(dat_str_alice)) | ~iext(uri_rdfs_range, Q_328, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_ex_name, Q_328)))).
% 12.11/4.08 tff(c_6663, plain, (![Q_32, D_358]: (iext(Q_32, D_358, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_358)))).
% 12.11/4.08 tff(c_6662, plain, (![C_28, D_358]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_358) | ~icext(uri_rdfs_Datatype, D_358)))).
% 12.11/4.08 tff(c_4048, plain, (![C_28, C_271]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_271) | ~iext(uri_rdfs_subClassOf, C_271, uri_rdf_Bag)))).
% 12.11/4.08 tff(c_8559, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_range))).
% 12.11/4.08 tff(c_8558, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_subject))).
% 12.11/4.08 tff(c_8557, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_rest))).
% 12.11/4.08 tff(c_8556, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_predicate))).
% 12.11/4.08 tff(c_8540, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_first))).
% 12.11/4.08 tff(c_5414, plain, (![Q_32, P_319]: (iext(Q_32, P_319, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_319, uri_rdfs_isDefinedBy)))).
% 12.11/4.08 tff(c_8539, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_domain))).
% 12.11/4.08 tff(c_8538, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_object))).
% 12.11/4.08 tff(c_5533, plain, (![C_13, Q_328]: (icext(C_13, uri_ex_alice) | ~iext(uri_rdfs_domain, Q_328, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_ex_name, Q_328)))).
% 12.11/4.08 tff(c_1481, plain, (![Q_80, D_11]: (iext(Q_80, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.08 tff(c_8450, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 12.11/4.08 tff(c_8449, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 12.11/4.08 tff(c_6301, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 12.11/4.08 tff(c_6334, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_5904, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 12.11/4.08 tff(c_5840, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 12.11/4.08 tff(c_1482, plain, (![Q_80, P_10]: (iext(Q_80, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_80) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.11/4.08 tff(c_5905, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_7733, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 12.11/4.08 tff(c_1583, plain, (![C_84, D_11]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_84, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.08 tff(c_7659, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 12.11/4.08 tff(c_1601, plain, (![P_87, P_10]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_87, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.11/4.08 tff(c_7626, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_rdfs_isDefinedBy))).
% 12.11/4.08 tff(c_5873, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_1483, plain, (![Q_80, X_7, C_8]: (iext(Q_80, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80) | ~icext(C_8, X_7)))).
% 12.11/4.08 tff(c_7610, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, uri_rdfs_isDefinedBy))).
% 12.11/4.08 tff(c_7609, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasValue, uri_rdfs_isDefinedBy))).
% 12.11/4.08 tff(c_5841, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_6265, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_5771, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Alt)))).
% 12.11/4.08 tff(c_1484, plain, (![Q_80, C_27]: (iext(Q_80, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80) | ~ic(C_27)))).
% 12.11/4.08 tff(c_6302, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.11/4.08 tff(c_7119, plain, (![C_72]: (icext(uri_rdfs_Class, C_72) | ~iext(uri_rdfs_range, uri_ex_name, C_72)))).
% 12.11/4.08 tff(c_7015, plain, (![C_362, X_363]: (icext(uri_rdfs_Class, C_362) | ~icext(C_362, X_363)))).
% 12.11/4.09 tff(c_1001, plain, (![C_72, C_8, X_7]: (icext(C_72, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_72) | ~icext(C_8, X_7)))).
% 12.11/4.09 tff(c_7011, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_6333, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_XMLLiteral)))).
% 12.11/4.09 tff(c_6676, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))).
% 12.11/4.09 tff(c_5780, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.09 tff(c_5799, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_5802, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_5796, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_5872, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_Bag)))).
% 12.11/4.09 tff(c_5793, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_5790, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_5787, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 12.11/4.09 tff(c_1585, plain, (![C_84, C_9]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, C_9) | ~ic(C_9)))).
% 12.11/4.09 tff(c_5718, plain, (![P_353]: (icext(uri_rdf_Property, P_353) | ~icext(uri_rdfs_ContainerMembershipProperty, P_353)))).
% 12.11/4.09 tff(c_1241, plain, (![C_76, P_10]: (icext(C_76, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.11/4.09 tff(c_1486, plain, (![Q_80, C_9]: (iext(Q_80, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80) | ~ic(C_9)))).
% 12.11/4.09 tff(c_5699, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_5687, plain, (![D_348]: (icext(uri_rdfs_Class, D_348) | ~icext(uri_rdfs_Datatype, D_348)))).
% 12.11/4.09 tff(c_1240, plain, (![C_76, D_11]: (icext(C_76, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.09 tff(c_1242, plain, (![C_76, X_7, C_8]: (icext(C_76, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76) | ~icext(C_8, X_7)))).
% 12.11/4.09 tff(c_1487, plain, (![Q_80, P_37]: (iext(Q_80, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_80) | ~ip(P_37)))).
% 12.11/4.09 tff(c_1485, plain, (![Q_80, P_6]: (iext(Q_80, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80) | ~ip(P_6)))).
% 12.11/4.09 tff(c_5648, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_1718, plain, (![D_24, P_92]: (icext(D_24, P_92) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_92)))).
% 12.11/4.09 tff(c_5618, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_5617, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_5616, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_1002, plain, (![C_72, C_27]: (icext(C_72, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72) | ~ic(C_27)))).
% 12.11/4.09 tff(c_5611, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 12.11/4.09 tff(c_835, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))).
% 12.11/4.09 tff(c_5575, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 12.11/4.09 tff(c_1005, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))).
% 12.11/4.09 tff(c_5548, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdf_type))).
% 12.11/4.09 tff(c_1246, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))).
% 12.11/4.09 tff(c_5542, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_subClassOf))).
% 12.11/4.09 tff(c_5541, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_rdfs_subPropertyOf))).
% 12.11/4.09 tff(c_1488, plain, (![Q_80]: (iext(Q_80, uri_ex_alice, literal_plain(dat_str_alice)) | ~iext(uri_rdfs_subPropertyOf, uri_ex_name, Q_80)))).
% 12.11/4.09 tff(c_1244, plain, (![C_76, P_6]: (icext(C_76, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76) | ~ip(P_6)))).
% 12.11/4.09 tff(c_5484, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1245, plain, (![C_76, C_9]: (icext(C_76, C_9) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76) | ~ic(C_9)))).
% 12.11/4.09 tff(c_834, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))).
% 12.11/4.09 tff(c_5454, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 12.11/4.09 tff(c_5453, plain, (~iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1554, plain, (![Q_80]: (iext(Q_80, '#skF_3', uri_rdf_nil) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_80)))).
% 12.11/4.09 tff(c_5422, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1513, plain, (![Q_80]: (iext(Q_80, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.09 tff(c_1603, plain, (![P_87]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))).
% 12.11/4.09 tff(c_5118, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1517, plain, (![Q_80]: (iext(Q_80, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.09 tff(c_5106, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 12.11/4.09 tff(c_5105, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 12.11/4.09 tff(c_5093, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1534, plain, (![Q_80]: (iext(Q_80, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.09 tff(c_5092, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 12.11/4.09 tff(c_1589, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Alt)))).
% 12.11/4.09 tff(c_1504, plain, (![Q_80]: (iext(Q_80, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.09 tff(c_1521, plain, (![Q_80]: (iext(Q_80, '#skF_2', uri_owl_FunctionalProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_80)))).
% 12.11/4.09 tff(c_1541, plain, (![Q_80]: (iext(Q_80, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.09 tff(c_1555, plain, (![Q_80]: (iext(Q_80, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.09 tff(c_4775, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_onProperty))).
% 12.11/4.09 tff(c_1540, plain, (![Q_80]: (iext(Q_80, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.09 tff(c_1529, plain, (![Q_80]: (iext(Q_80, '#skF_4', uri_rdfs_domain) | ~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_80)))).
% 12.11/4.09 tff(c_1518, plain, (![Q_80]: (iext(Q_80, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.09 tff(c_1507, plain, (![Q_80]: (iext(Q_80, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.09 tff(c_4741, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_hasValue))).
% 12.11/4.10 tff(c_1505, plain, (![Q_80]: (iext(Q_80, '#skF_4', uri_foaf_Person) | ~iext(uri_rdfs_subPropertyOf, uri_owl_hasValue, Q_80)))).
% 12.11/4.10 tff(c_1509, plain, (![Q_80]: (iext(Q_80, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_1489, plain, (![Q_80]: (iext(Q_80, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1508, plain, (![Q_80]: (iext(Q_80, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_4696, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 12.11/4.10 tff(c_1538, plain, (![Q_80]: (iext(Q_80, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_80)))).
% 12.11/4.10 tff(c_1588, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Seq)))).
% 12.11/4.10 tff(c_1491, plain, (![Q_80]: (iext(Q_80, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_4654, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.10 tff(c_1537, plain, (![Q_80]: (iext(Q_80, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4653, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdfs_Class))).
% 12.11/4.10 tff(c_4652, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdfs_Literal))).
% 12.11/4.10 tff(c_4651, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdfs_Datatype))).
% 12.11/4.10 tff(c_4650, plain, (~iext(uri_rdfs_range, uri_ex_name, uri_rdf_Property))).
% 12.11/4.10 tff(c_1006, plain, (![C_72]: (icext(C_72, literal_plain(dat_str_alice)) | ~iext(uri_rdfs_range, uri_ex_name, C_72)))).
% 12.11/4.10 tff(c_1497, plain, (![Q_80]: (iext(Q_80, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_1499, plain, (![Q_80]: (iext(Q_80, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4598, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_intersectionOf))).
% 12.11/4.10 tff(c_1558, plain, (![Q_80]: (iext(Q_80, uri_ex_PersonAttribute, '#skF_1') | ~iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, Q_80)))).
% 12.11/4.10 tff(c_1531, plain, (![Q_80]: (iext(Q_80, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_1559, plain, (![Q_80]: (iext(Q_80, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1527, plain, (![Q_80]: (iext(Q_80, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_1552, plain, (![Q_80]: (iext(Q_80, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1544, plain, (![Q_80]: (iext(Q_80, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_1526, plain, (![Q_80]: (iext(Q_80, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.10 tff(c_1586, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_ContainerMembershipProperty)))).
% 12.11/4.10 tff(c_1498, plain, (![Q_80]: (iext(Q_80, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_1528, plain, (![Q_80]: (iext(Q_80, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1494, plain, (![Q_80]: (iext(Q_80, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_4468, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1512, plain, (![Q_80]: (iext(Q_80, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1553, plain, (![Q_80]: (iext(Q_80, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4456, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Bag))).
% 12.11/4.10 tff(c_1500, plain, (![Q_80]: (iext(Q_80, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4444, plain, (~iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, uri_rdf_Bag))).
% 12.11/4.10 tff(c_4432, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1503, plain, (![Q_80]: (iext(Q_80, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_4420, plain, (~iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1515, plain, (![Q_80]: (iext(Q_80, uri_foaf_Person, uri_owl_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_4419, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Bag))).
% 12.11/4.10 tff(c_1493, plain, (![Q_80]: (iext(Q_80, uri_ex_name, uri_ex_PersonAttribute) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_4396, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1549, plain, (![Q_80]: (iext(Q_80, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4395, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 12.11/4.10 tff(c_4383, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1522, plain, (![Q_80]: (iext(Q_80, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.10 tff(c_4371, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1547, plain, (![Q_80]: (iext(Q_80, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_4370, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 12.11/4.10 tff(c_4369, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1557, plain, (![Q_80]: (iext(Q_80, '#skF_1', '#skF_2') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_80)))).
% 12.11/4.10 tff(c_4357, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_4345, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 12.11/4.10 tff(c_1495, plain, (![Q_80]: (iext(Q_80, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_4344, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_rest))).
% 12.11/4.10 tff(c_4332, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 12.11/4.10 tff(c_1551, plain, (![Q_80]: (iext(Q_80, '#skF_2', '#skF_3') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_80)))).
% 12.11/4.10 tff(c_4331, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 12.11/4.10 tff(c_1590, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_XMLLiteral)))).
% 12.11/4.10 tff(c_4069, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 12.11/4.10 tff(c_4068, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 12.11/4.10 tff(c_1543, plain, (![Q_80]: (iext(Q_80, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_1587, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Bag)))).
% 12.11/4.10 tff(c_1548, plain, (![Q_80]: (iext(Q_80, '#skF_3', '#skF_4') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_80)))).
% 12.11/4.10 tff(c_1536, plain, (![Q_80]: (iext(Q_80, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.10 tff(c_1591, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Datatype)))).
% 12.11/4.10 tff(c_1524, plain, (![Q_80]: (iext(Q_80, '#skF_4', uri_owl_Restriction) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1530, plain, (![Q_80]: (iext(Q_80, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_1514, plain, (![Q_80]: (iext(Q_80, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.10 tff(c_1510, plain, (![Q_80]: (iext(Q_80, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1523, plain, (![Q_80]: (iext(Q_80, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.10 tff(c_1550, plain, (![Q_80]: (iext(Q_80, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_3699, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_first))).
% 12.11/4.10 tff(c_1533, plain, (![Q_80]: (iext(Q_80, '#skF_1', uri_owl_DatatypeProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_80)))).
% 12.11/4.10 tff(c_1511, plain, (![Q_80]: (iext(Q_80, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.10 tff(c_1539, plain, (![Q_80]: (iext(Q_80, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.10 tff(c_1520, plain, (![Q_80]: (iext(Q_80, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_1545, plain, (![Q_80]: (iext(Q_80, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.11 tff(c_1525, plain, (![Q_80]: (iext(Q_80, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_1502, plain, (![Q_80]: (iext(Q_80, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.11 tff(c_1546, plain, (![Q_80]: (iext(Q_80, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_3610, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 12.11/4.11 tff(c_1501, plain, (![Q_80]: (iext(Q_80, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_80)))).
% 12.11/4.11 tff(c_1492, plain, (![Q_80]: (iext(Q_80, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_1556, plain, (![Q_80]: (iext(Q_80, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.11 tff(c_1519, plain, (![Q_80]: (iext(Q_80, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_1820, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1788, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2037, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1849, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1898, plain, (![D_24]: (icext(D_24, '#skF_3') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 12.11/4.11 tff(c_1878, plain, (![D_24]: (icext(D_24, '#skF_2') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 12.11/4.11 tff(c_1799, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1506, plain, (![Q_80]: (iext(Q_80, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_2133, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1956, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 12.11/4.11 tff(c_1928, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1831, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_2174, plain, (![D_24]: (icext(D_24, uri_ex_PersonAttribute) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1999, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1889, plain, (![D_24]: (icext(D_24, uri_owl_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_2018, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1862, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1542, plain, (![Q_80]: (iext(Q_80, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.11 tff(c_2089, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1948, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2050, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1988, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2290, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_2475, plain, (![D_24]: (icext(D_24, uri_owl_Restriction) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_2064, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2199, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_2279, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1535, plain, (![Q_80]: (iext(Q_80, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.11 tff(c_2353, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2421, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2303, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1650, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.11/4.11 tff(c_2947, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 12.11/4.11 tff(c_1638, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1659, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.11/4.11 tff(c_2890, plain, (~icext(uri_rdfs_Datatype, uri_owl_Restriction))).
% 12.11/4.11 tff(c_1496, plain, (![Q_80]: (iext(Q_80, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_80)))).
% 12.11/4.11 tff(c_1653, plain, (![D_24]: (icext(D_24, '#skF_4') | ~iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_24)))).
% 12.11/4.11 tff(c_2869, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 12.11/4.11 tff(c_1635, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1626, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1647, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1632, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1644, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_1516, plain, (![Q_80]: (iext(Q_80, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_80)))).
% 12.11/4.11 tff(c_1620, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2737, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 12.11/4.11 tff(c_1623, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 12.11/4.11 tff(c_2716, plain, (~icext(uri_rdfs_Datatype, uri_ex_PersonAttribute))).
% 12.11/4.11 tff(c_1662, plain, (![D_24]: (icext(D_24, uri_ex_name) | ~iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, D_24)))).
% 12.11/4.11 tff(c_2695, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 12.11/4.11 tff(c_1490, plain, (![Q_80]: (iext(Q_80, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.11 tff(c_1617, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 12.11/4.11 tff(c_1673, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2638, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 12.11/4.11 tff(c_2617, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 12.11/4.11 tff(c_1629, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.11/4.11 tff(c_2616, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.11 tff(c_1532, plain, (![Q_80]: (iext(Q_80, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_80)))).
% 12.11/4.11 tff(c_1641, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.11/4.11 tff(c_2579, plain, (~icext(uri_rdfs_Datatype, uri_owl_Class))).
% 12.11/4.11 tff(c_1656, plain, (![D_24]: (icext(D_24, uri_foaf_Person) | ~iext(uri_rdfs_subClassOf, uri_owl_Class, D_24)))).
% 12.11/4.11 tff(c_2558, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 12.11/4.11 tff(c_1668, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.11/4.11 tff(c_1255, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.11 tff(c_1291, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.11 tff(c_1247, plain, (![C_76]: (icext(C_76, uri_ex_alice) | ~iext(uri_rdfs_domain, uri_ex_name, C_76)))).
% 12.11/4.11 tff(c_1259, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.11 tff(c_1278, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.11 tff(c_1297, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76)))).
% 12.11/4.11 tff(c_1258, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.11 tff(c_1019, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 12.11/4.11 tff(c_1279, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1072, plain, (![C_72]: (icext(C_72, uri_rdf_nil) | ~iext(uri_rdfs_range, uri_rdf_rest, C_72)))).
% 12.11/4.12 tff(c_1272, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_2476, plain, (ic(uri_owl_Restriction))).
% 12.11/4.12 tff(c_2469, plain, (icext(uri_rdfs_Class, uri_owl_Restriction))).
% 12.11/4.12 tff(c_1042, plain, (![C_72]: (icext(C_72, uri_owl_Restriction) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1074, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1039, plain, (![C_72]: (icext(C_72, uri_owl_FunctionalProperty) | ~iext(uri_rdfs_range, uri_rdf_first, C_72)))).
% 12.11/4.12 tff(c_1301, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1250, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1046, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1257, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1289, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1023, plain, (![C_72]: (icext(C_72, uri_foaf_Person) | ~iext(uri_rdfs_range, uri_owl_hasValue, C_72)))).
% 12.11/4.12 tff(c_2413, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 12.11/4.12 tff(c_1263, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_2408, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 12.11/4.12 tff(c_836, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))).
% 12.11/4.12 tff(c_1302, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1265, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1256, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1253, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1047, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_range, uri_owl_onProperty, C_72)))).
% 12.11/4.12 tff(c_1270, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1016, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 12.11/4.12 tff(c_2352, plain, (ip(uri_rdfs_label))).
% 12.11/4.12 tff(c_2346, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 12.11/4.12 tff(c_1296, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1299, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1308, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1254, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1251, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1276, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1274, plain, (![C_76]: (icext(C_76, uri_foaf_Person) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_2297, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.12 tff(c_1260, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.12 tff(c_2284, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 12.11/4.12 tff(c_1295, plain, (![C_76]: (icext(C_76, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.12 tff(c_2278, plain, (ip(uri_rdfs_comment))).
% 12.11/4.12 tff(c_2272, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 12.11/4.12 tff(c_1262, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1057, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 12.11/4.12 tff(c_1311, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1303, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1063, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 12.11/4.12 tff(c_1062, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 12.11/4.12 tff(c_1300, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1318, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1283, plain, (![C_76]: (icext(C_76, '#skF_4') | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1022, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 12.11/4.12 tff(c_1305, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1252, plain, (![C_76]: (icext(C_76, uri_ex_name) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_2193, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 12.11/4.12 tff(c_1298, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.12 tff(c_1051, plain, (![C_72]: (icext(C_72, uri_owl_DatatypeProperty) | ~iext(uri_rdfs_range, uri_rdf_first, C_72)))).
% 12.11/4.12 tff(c_1313, plain, (![C_76]: (icext(C_76, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_76)))).
% 12.11/4.12 tff(c_2175, plain, (ic(uri_ex_PersonAttribute))).
% 12.11/4.12 tff(c_1076, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_range, uri_owl_intersectionOf, C_72)))).
% 12.11/4.12 tff(c_2168, plain, (icext(uri_rdfs_Class, uri_ex_PersonAttribute))).
% 12.11/4.12 tff(c_1011, plain, (![C_72]: (icext(C_72, uri_ex_PersonAttribute) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1294, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1310, plain, (![C_76]: (icext(C_76, '#skF_2') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_76)))).
% 12.11/4.12 tff(c_1309, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1066, plain, (![C_72]: (icext(C_72, '#skF_4') | ~iext(uri_rdfs_range, uri_rdf_first, C_72)))).
% 12.11/4.12 tff(c_1292, plain, (![C_76]: (icext(C_76, '#skF_1') | ~iext(uri_rdfs_domain, uri_rdf_first, C_76)))).
% 12.11/4.12 tff(c_2119, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 12.11/4.12 tff(c_1075, plain, (![C_72]: (icext(C_72, '#skF_2') | ~iext(uri_rdfs_range, uri_rdf_rest, C_72)))).
% 12.11/4.12 tff(c_1314, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1248, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1287, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1304, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.12 tff(c_1264, plain, (![C_76]: (icext(C_76, '#skF_4') | ~iext(uri_rdfs_domain, uri_owl_hasValue, C_76)))).
% 12.11/4.12 tff(c_1312, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_2081, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 12.11/4.12 tff(c_1266, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1069, plain, (![C_72]: (icext(C_72, '#skF_3') | ~iext(uri_rdfs_range, uri_rdf_rest, C_72)))).
% 12.11/4.12 tff(c_1073, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 12.11/4.12 tff(c_2063, plain, (ip(uri_rdf_predicate))).
% 12.11/4.12 tff(c_2057, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 12.11/4.12 tff(c_1249, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_2044, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 12.11/4.12 tff(c_1055, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 12.11/4.12 tff(c_2031, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 12.11/4.12 tff(c_1052, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1268, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_2012, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 12.11/4.12 tff(c_1285, plain, (![C_76]: (icext(C_76, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.12 tff(c_1293, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1993, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 12.11/4.12 tff(c_1053, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1980, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 12.11/4.12 tff(c_1286, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.12 tff(c_1315, plain, (![C_76]: (icext(C_76, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1288, plain, (![C_76]: (icext(C_76, '#skF_4') | ~iext(uri_rdfs_domain, uri_owl_onProperty, C_76)))).
% 12.11/4.12 tff(c_1290, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1306, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 12.11/4.12 tff(c_1953, plain, (icext(uri_rdf_List, '#skF_1'))).
% 12.11/4.12 tff(c_1316, plain, (![C_76]: (icext(C_76, '#skF_1') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_76)))).
% 12.11/4.12 tff(c_1940, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 12.11/4.12 tff(c_1056, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))).
% 12.11/4.12 tff(c_1282, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.12 tff(c_1929, plain, (ic(uri_rdfs_Statement))).
% 12.11/4.12 tff(c_1922, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 12.11/4.12 tff(c_1009, plain, (![C_72]: (icext(C_72, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 12.11/4.12 tff(c_1061, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 12.11/4.12 tff(c_1317, plain, (![C_76]: (icext(C_76, uri_ex_PersonAttribute) | ~iext(uri_rdfs_domain, uri_owl_intersectionOf, C_76)))).
% 12.11/4.12 tff(c_1036, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.12 tff(c_1277, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 12.11/4.13 tff(c_1895, plain, (icext(uri_rdf_List, '#skF_3'))).
% 12.11/4.13 tff(c_1307, plain, (![C_76]: (icext(C_76, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_first, C_76)))).
% 12.11/4.13 tff(c_1890, plain, (ic(uri_owl_Class))).
% 12.11/4.13 tff(c_1883, plain, (icext(uri_rdfs_Class, uri_owl_Class))).
% 12.11/4.13 tff(c_1033, plain, (![C_72]: (icext(C_72, uri_owl_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 12.11/4.13 tff(c_1875, plain, (icext(uri_rdf_List, '#skF_2'))).
% 12.11/4.13 tff(c_1280, plain, (![C_76]: (icext(C_76, '#skF_2') | ~iext(uri_rdfs_domain, uri_rdf_first, C_76)))).
% 12.11/4.13 tff(c_1050, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 12.11/4.13 tff(c_1856, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 12.11/4.13 tff(c_1281, plain, (![C_76]: (icext(C_76, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 12.11/4.13 tff(c_1843, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_1043, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 12.11/4.13 tff(c_1832, plain, (ic(uri_rdf_List))).
% 12.11/4.13 tff(c_1273, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.13 tff(c_1825, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 12.11/4.13 tff(c_1060, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 12.11/4.13 tff(c_1812, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 12.11/4.13 tff(c_1267, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.13 tff(c_1284, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.13 tff(c_1793, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 12.11/4.13 tff(c_1040, plain, (![C_72]: (icext(C_72, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 12.11/4.13 tff(c_1780, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 12.11/4.13 tff(c_1275, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 12.11/4.13 tff(c_781, plain, (![X_65]: (ip(X_65) | ~icext(uri_rdf_Property, X_65)))).
% 12.11/4.13 tff(c_1724, plain, (ip(uri_rdfs_member))).
% 12.11/4.13 tff(c_742, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 12.11/4.13 tff(c_801, plain, (![P_67]: (ip(P_67) | ~icext(uri_rdfs_ContainerMembershipProperty, P_67)))).
% 12.11/4.13 tff(c_819, plain, (![D_68]: (ic(D_68) | ~icext(uri_rdfs_Datatype, D_68)))).
% 12.11/4.13 tff(c_1692, plain, (ic(uri_rdfs_Resource))).
% 12.11/4.13 tff(c_753, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 12.11/4.13 tff(c_757, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 12.11/4.13 tff(c_744, plain, (icext(uri_ex_PersonAttribute, uri_ex_name))).
% 12.11/4.13 tff(c_743, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 12.11/4.13 tff(c_751, plain, (icext(uri_owl_Class, uri_foaf_Person))).
% 12.11/4.13 tff(c_754, plain, (icext(uri_owl_Restriction, '#skF_4'))).
% 12.11/4.13 tff(c_758, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 12.11/4.13 tff(c_752, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 12.11/4.13 tff(c_748, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 12.11/4.13 tff(c_755, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 12.11/4.13 tff(c_747, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 12.11/4.13 tff(c_749, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 12.11/4.13 tff(c_745, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 12.11/4.13 tff(c_760, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 12.11/4.13 tff(c_750, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 12.11/4.13 tff(c_759, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 12.11/4.13 tff(c_746, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 12.11/4.13 tff(c_756, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 12.11/4.13 tff(c_538, plain, (ic(uri_rdfs_Seq))).
% 12.11/4.13 tff(c_462, plain, (ip(uri_owl_hasValue))).
% 12.11/4.13 tff(c_574, plain, (ip(uri_rdf__1))).
% 12.11/4.13 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)))).
% 12.11/4.13 tff(c_495, plain, (ip(uri_rdfs_subPropertyOf))).
% 12.11/4.13 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)))).
% 12.11/4.13 tff(c_539, plain, (ic(uri_rdf_Alt))).
% 12.11/4.13 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)))).
% 12.11/4.13 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)))).
% 12.11/4.13 tff(c_537, plain, (ic(uri_rdf_Bag))).
% 12.11/4.13 tff(c_576, plain, (ip(uri_rdf__2))).
% 12.11/4.13 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)))).
% 12.11/4.13 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)))).
% 12.11/4.13 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.11/4.13 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.11/4.13 tff(c_784, plain, (~icext(uri_owl_FunctionalProperty, uri_ex_name))).
% 12.11/4.13 tff(c_620, plain, (ic(uri_rdf_Property))).
% 12.11/4.13 tff(c_486, plain, (ip(uri_owl_onProperty))).
% 12.11/4.13 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 12.11/4.13 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 12.11/4.13 tff(c_681, plain, (ip(uri_rdfs_isDefinedBy))).
% 12.11/4.13 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 12.11/4.13 tff(c_502, plain, (ip(uri_rdfs_subClassOf))).
% 12.11/4.13 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 12.11/4.13 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 12.11/4.13 tff(c_622, plain, (ic(uri_rdfs_Container))).
% 12.11/4.13 tff(c_512, plain, (ip(uri_rdfs_range))).
% 12.11/4.13 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 12.11/4.13 tff(c_624, plain, (ic(uri_rdfs_Literal))).
% 12.11/4.13 tff(c_625, plain, (ic(uri_rdfs_Class))).
% 12.11/4.13 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 12.11/4.13 tff(c_536, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.13 tff(c_597, plain, (ip(uri_rdfs_seeAlso))).
% 12.11/4.13 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 12.11/4.13 tff(c_575, plain, (ip(uri_rdf__3))).
% 12.11/4.13 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 12.11/4.13 tff(c_577, plain, (ip(uri_rdf_subject))).
% 12.11/4.13 tff(c_578, plain, (ip(uri_rdf_value))).
% 12.11/4.13 tff(c_579, plain, (ip(uri_rdf_object))).
% 12.11/4.13 tff(c_580, plain, (ip(uri_rdf_first))).
% 12.11/4.13 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 12.11/4.13 tff(c_540, plain, (ic(uri_rdf_XMLLiteral))).
% 12.11/4.13 tff(c_541, plain, (ic(uri_rdfs_Datatype))).
% 12.11/4.13 tff(c_473, plain, (ip(uri_rdfs_domain))).
% 12.11/4.13 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 12.11/4.13 tff(c_514, plain, (ip(uri_rdf_rest))).
% 12.11/4.13 tff(c_515, plain, (ip(uri_owl_intersectionOf))).
% 12.11/4.13 tff(c_516, plain, (ip(uri_rdf_type))).
% 12.11/4.13 tff(c_445, plain, (ip(uri_ex_name))).
% 12.11/4.13 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 12.11/4.13 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 12.11/4.13 tff(c_182, plain, (iext(uri_ex_name, uri_ex_alice, literal_plain(dat_str_alice)))).
% 12.11/4.13 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 12.11/4.13 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 12.11/4.13 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 12.11/4.13 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.13 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 12.11/4.13 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 12.11/4.13 tff(c_184, plain, (iext(uri_rdf_type, uri_ex_name, uri_ex_PersonAttribute))).
% 12.11/4.13 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 12.11/4.13 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 12.11/4.13 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 12.11/4.13 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 12.11/4.13 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 12.11/4.13 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 12.11/4.13 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 12.11/4.13 tff(c_186, plain, (iext(uri_owl_hasValue, '#skF_4', uri_foaf_Person))).
% 12.11/4.13 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 12.11/4.13 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 12.11/4.13 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 12.11/4.13 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 12.11/4.13 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 12.11/4.13 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 12.11/4.13 tff(c_206, plain, (iext(uri_rdf_type, uri_foaf_Person, uri_owl_Class))).
% 12.11/4.13 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 12.11/4.13 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 12.11/4.13 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 12.11/4.14 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_198, plain, (iext(uri_rdf_first, '#skF_2', uri_owl_FunctionalProperty))).
% 12.11/4.14 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 12.11/4.14 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 12.11/4.14 tff(c_190, plain, (iext(uri_rdf_type, '#skF_4', uri_owl_Restriction))).
% 12.11/4.14 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 12.11/4.14 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 12.11/4.14 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.14 tff(c_188, plain, (iext(uri_owl_onProperty, '#skF_4', uri_rdfs_domain))).
% 12.11/4.14 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 12.11/4.14 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 12.11/4.14 tff(c_202, plain, (iext(uri_rdf_first, '#skF_1', uri_owl_DatatypeProperty))).
% 12.11/4.14 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 12.11/4.14 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 12.11/4.14 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 12.11/4.14 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 12.11/4.14 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 12.11/4.14 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 12.11/4.14 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 12.11/4.14 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_215, plain, (~iext(uri_rdf_type, uri_ex_name, uri_owl_FunctionalProperty))).
% 12.11/4.14 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 12.11/4.14 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 12.11/4.14 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_194, plain, (iext(uri_rdf_first, '#skF_3', '#skF_4'))).
% 12.11/4.14 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 12.11/4.14 tff(c_196, plain, (iext(uri_rdf_rest, '#skF_2', '#skF_3'))).
% 12.11/4.14 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 12.11/4.14 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 12.11/4.14 tff(c_192, plain, (iext(uri_rdf_rest, '#skF_3', uri_rdf_nil))).
% 12.11/4.14 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 12.11/4.14 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 12.11/4.14 tff(c_200, plain, (iext(uri_rdf_rest, '#skF_1', '#skF_2'))).
% 12.11/4.14 tff(c_204, plain, (iext(uri_owl_intersectionOf, uri_ex_PersonAttribute, '#skF_1'))).
% 12.11/4.14 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 12.11/4.14 tff(c_210, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 12.11/4.14 tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 12.11/4.14 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.11/4.14
%------------------------------------------------------------------------------