↑ Up

Beagle---0.9.52.SAT-Ass.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : SWB019+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 : n031.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Apr  9 09:15:53 PM UTC 2025

% Result   : Satisfiable 13.16s 4.36s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB019+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 : n031.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:58:52 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 13.16/4.36  
% 13.16/4.36  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.16/4.36  
% 13.16/4.36  % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.16/4.37  %$ iext > icext > lv > ir > ip > ic > #nlpp > literal_plain > uri_skos_prefLabel > uri_skos_altLabel > 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_propertyDisjointWith > uri_owl_AnnotationProperty > uri_ex_foo > dat_str_foo
% 13.16/4.37  
% 13.16/4.37  %Foreground sorts:
% 13.16/4.37  
% 13.16/4.37  
% 13.16/4.37  %Background operators:
% 13.16/4.37  
% 13.16/4.37  
% 13.16/4.37  %Foreground operators:
% 13.16/4.37  tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 13.16/4.37  tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 13.16/4.37  tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 13.16/4.37  tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 13.16/4.37  tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 13.16/4.37  tff(uri_rdf_type, type, uri_rdf_type: $i).
% 13.16/4.37  tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 13.16/4.37  tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 13.16/4.37  tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 13.16/4.37  tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 13.16/4.37  tff(uri_rdf_List, type, uri_rdf_List: $i).
% 13.16/4.37  tff(uri_rdf_first, type, uri_rdf_first: $i).
% 13.16/4.37  tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 13.16/4.37  tff(uri_skos_altLabel, type, uri_skos_altLabel: $i).
% 13.16/4.37  tff(uri_owl_propertyDisjointWith, type, uri_owl_propertyDisjointWith: $i).
% 13.16/4.37  tff(uri_rdf__3, type, uri_rdf__3: $i).
% 13.16/4.37  tff(icext, type, icext: ($i * $i) > $o).
% 13.16/4.37  tff(uri_rdf_value, type, uri_rdf_value: $i).
% 13.16/4.37  tff(ip, type, ip: $i > $o).
% 13.16/4.37  tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 13.16/4.37  tff(dat_str_foo, type, dat_str_foo: $i).
% 13.16/4.37  tff(uri_rdf__1, type, uri_rdf__1: $i).
% 13.16/4.37  tff(lv, type, lv: $i > $o).
% 13.16/4.37  tff(ir, type, ir: $i > $o).
% 13.16/4.37  tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 13.16/4.37  tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 13.16/4.37  tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 13.16/4.37  tff(ic, type, ic: $i > $o).
% 13.16/4.37  tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 13.16/4.37  tff(uri_rdf_object, type, uri_rdf_object: $i).
% 13.16/4.37  tff(uri_owl_AnnotationProperty, type, uri_owl_AnnotationProperty: $i).
% 13.16/4.37  tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 13.16/4.37  tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 13.16/4.37  tff(iext, type, iext: ($i * $i * $i) > $o).
% 13.16/4.37  tff(uri_skos_prefLabel, type, uri_skos_prefLabel: $i).
% 13.16/4.37  tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 13.16/4.37  tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 13.16/4.37  tff(uri_rdf__2, type, uri_rdf__2: $i).
% 13.16/4.37  tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 13.16/4.37  tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 13.16/4.37  tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 13.16/4.37  tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 13.16/4.37  tff(uri_ex_foo, type, uri_ex_foo: $i).
% 13.16/4.37  tff(literal_plain, type, literal_plain: $i > $i).
% 13.16/4.37  tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 13.16/4.37  tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 13.16/4.37  
% 13.16/4.37  %Saturated clause set:
% 13.16/4.37  tff(c_10691, plain, (![P_83]: (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, P_83) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_isDefinedBy)))).
% 13.16/4.37  tff(c_10637, plain, (![C_80]: (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.16/4.37  tff(c_10618, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.16/4.37  tff(c_10564, plain, (![C_80]: (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 13.16/4.37  tff(c_10555, plain, (![C_80]: (~iext(uri_rdfs_range, uri_rdfs_label, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.16/4.37  tff(c_10509, plain, (![C_80]: (~iext(uri_rdfs_range, uri_rdfs_label, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 13.16/4.37  tff(c_9584, plain, (![Q_32, Q_422]: (iext(Q_32, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, Q_422, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, Q_422)))).
% 13.16/4.37  tff(c_10508, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdf_Bag))).
% 13.16/4.38  tff(c_10507, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdf_Alt))).
% 13.16/4.38  tff(c_10506, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Seq))).
% 13.16/4.38  tff(c_10404, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Seq))).
% 13.16/4.38  tff(c_9429, plain, (![D_24, C_418]: (icext(D_24, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subClassOf, C_418, D_24) | ~iext(uri_rdfs_range, uri_rdfs_label, C_418)))).
% 13.16/4.38  tff(c_8835, plain, (![D_24, D_395]: (icext(D_24, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subClassOf, D_395, D_24) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_395)))).
% 13.16/4.38  tff(c_10284, plain, (![P_83]: (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, P_83) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_isDefinedBy)))).
% 13.16/4.38  tff(c_9588, plain, (![C_20, Q_422]: (icext(C_20, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, Q_422, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, Q_422)))).
% 13.16/4.38  tff(c_7416, plain, (![Q_32, C_345]: (iext(Q_32, C_345, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_345, uri_rdfs_Datatype)))).
% 13.16/4.38  tff(c_7733, plain, (![C_28, C_347]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_347) | ~iext(uri_rdfs_subClassOf, C_347, uri_rdfs_ContainerMembershipProperty)))).
% 13.16/4.38  tff(c_7732, plain, (![Q_32, C_347]: (iext(Q_32, C_347, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_347, uri_rdfs_ContainerMembershipProperty)))).
% 13.16/4.38  tff(c_10056, plain, (![P_83]: (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, P_83) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_isDefinedBy)))).
% 13.16/4.38  tff(c_6473, plain, (![C_28, C_337]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_337) | ~iext(uri_rdfs_subClassOf, C_337, uri_rdf_Bag)))).
% 13.16/4.38  tff(c_6472, plain, (![Q_32, C_337]: (iext(Q_32, C_337, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_337, uri_rdf_Bag)))).
% 13.16/4.38  tff(c_7417, plain, (![C_28, C_345]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_345) | ~iext(uri_rdfs_subClassOf, C_345, uri_rdfs_Datatype)))).
% 13.16/4.38  tff(c_7112, plain, (![Q_32, C_344]: (iext(Q_32, C_344, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_344, uri_rdf_Alt)))).
% 13.16/4.38  tff(c_9825, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_skos_prefLabel))).
% 13.16/4.38  tff(c_9805, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.16/4.38  tff(c_7113, plain, (![C_28, C_344]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_344) | ~iext(uri_rdfs_subClassOf, C_344, uri_rdf_Alt)))).
% 13.16/4.38  tff(c_9707, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_domain))).
% 13.16/4.38  tff(c_9706, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_subject))).
% 13.16/4.38  tff(c_9704, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_skos_altLabel))).
% 13.16/4.38  tff(c_9683, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.16/4.38  tff(c_9682, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_range))).
% 13.16/4.38  tff(c_9681, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_rest))).
% 13.16/4.38  tff(c_9680, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_first))).
% 13.16/4.38  tff(c_9679, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_object))).
% 13.16/4.38  tff(c_9678, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_predicate))).
% 13.16/4.38  tff(c_9587, plain, (![C_13, Q_422]: (icext(C_13, uri_ex_foo) | ~iext(uri_rdfs_domain, Q_422, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, Q_422)))).
% 13.16/4.38  tff(c_9597, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdf_type))).
% 13.16/4.38  tff(c_9596, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_subPropertyOf))).
% 13.16/4.38  tff(c_9595, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_subClassOf))).
% 13.16/4.38  tff(c_9364, plain, (![Q_32]: (iext(Q_32, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, Q_32)))).
% 13.16/4.38  tff(c_9479, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_isDefinedBy))).
% 13.16/4.38  tff(c_9478, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_isDefinedBy))).
% 13.16/4.38  tff(c_9477, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Datatype))).
% 13.16/4.38  tff(c_9476, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdf_Property))).
% 13.16/4.38  tff(c_9474, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Class))).
% 13.16/4.38  tff(c_9473, plain, (~iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_ContainerMembershipProperty))).
% 13.16/4.38  tff(c_5244, plain, (![Q_32, Q_307]: (iext(Q_32, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, Q_307, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, Q_307)))).
% 13.16/4.38  tff(c_9423, plain, (![C_418]: (icext(uri_rdfs_Class, C_418) | ~iext(uri_rdfs_range, uri_rdfs_label, C_418)))).
% 13.16/4.38  tff(c_9366, plain, (![C_20]: (icext(C_20, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, uri_rdfs_label, C_20)))).
% 13.16/4.38  tff(c_9339, plain, (![Q_32]: (iext(Q_32, uri_skos_prefLabel, uri_skos_prefLabel) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32)))).
% 13.16/4.38  tff(c_9365, plain, (![C_13]: (icext(C_13, uri_ex_foo) | ~iext(uri_rdfs_domain, uri_rdfs_label, C_13)))).
% 13.16/4.38  tff(c_9304, plain, (iext(uri_rdfs_label, uri_ex_foo, literal_plain(dat_str_foo)))).
% 13.16/4.38  tff(c_9342, plain, (![C_20]: (icext(C_20, uri_skos_prefLabel) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_20)))).
% 13.16/4.38  tff(c_9305, plain, (iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_skos_prefLabel))).
% 13.16/4.38  tff(c_5152, plain, (![Q_32, Q_300]: (iext(Q_32, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, Q_300, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, Q_300)))).
% 13.16/4.38  tff(c_9259, plain, (![C_80]: (~iext(uri_rdfs_range, uri_skos_prefLabel, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 13.16/4.38  tff(c_6778, plain, (![Q_32, C_340]: (iext(Q_32, C_340, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_340, uri_rdf_XMLLiteral)))).
% 13.16/4.38  tff(c_9235, plain, (![C_80]: (~iext(uri_rdfs_range, uri_skos_altLabel, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.16/4.38  tff(c_9226, plain, (![C_80]: (~iext(uri_rdfs_range, uri_skos_altLabel, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 13.16/4.38  tff(c_9216, plain, (![C_80]: (~iext(uri_rdfs_range, uri_skos_prefLabel, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.16/4.38  tff(c_6779, plain, (![C_28, C_340]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_340) | ~iext(uri_rdfs_subClassOf, C_340, uri_rdf_XMLLiteral)))).
% 13.16/4.38  tff(c_9122, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 13.16/4.38  tff(c_3874, plain, (![Q_32, C_239]: (iext(Q_32, C_239, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_239, uri_rdf_Bag)))).
% 13.16/4.38  tff(c_9106, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_isDefinedBy))).
% 13.16/4.38  tff(c_4774, plain, (![P_38, P_278]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_278) | ~iext(uri_rdfs_subPropertyOf, P_278, uri_rdfs_isDefinedBy)))).
% 13.16/4.38  tff(c_9077, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_ContainerMembershipProperty))).
% 13.16/4.38  tff(c_5248, plain, (![C_20, Q_307]: (icext(C_20, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, Q_307, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, Q_307)))).
% 13.16/4.39  tff(c_9000, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Datatype))).
% 13.16/4.39  tff(c_8829, plain, (![D_395]: (icext(uri_rdfs_Class, D_395) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_395)))).
% 13.16/4.39  tff(c_8923, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Property))).
% 13.16/4.39  tff(c_8924, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 13.16/4.39  tff(c_8922, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Class))).
% 13.16/4.39  tff(c_4397, plain, (![C_28, C_265]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_265) | ~iext(uri_rdfs_subClassOf, C_265, uri_rdf_XMLLiteral)))).
% 13.16/4.39  tff(c_8793, plain, (![D_24]: (icext(D_24, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_24)))).
% 13.16/4.39  tff(c_8794, plain, (lv(literal_plain(dat_str_foo)))).
% 13.16/4.39  tff(c_8769, plain, (icext(uri_rdfs_Literal, literal_plain(dat_str_foo)))).
% 13.16/4.39  tff(c_5156, plain, (![C_20, Q_300]: (icext(C_20, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, Q_300, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, Q_300)))).
% 13.16/4.39  tff(c_3554, plain, (![Q_32, C_231]: (iext(Q_32, C_231, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_231, uri_rdf_Alt)))).
% 13.16/4.39  tff(c_3555, plain, (![C_28, C_231]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_231) | ~iext(uri_rdfs_subClassOf, C_231, uri_rdf_Alt)))).
% 13.16/4.39  tff(c_8605, plain, (![D_11]: (~iext(uri_rdfs_range, uri_skos_prefLabel, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.16/4.39  tff(c_4396, plain, (![Q_32, C_265]: (iext(Q_32, C_265, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_265, uri_rdf_XMLLiteral)))).
% 13.16/4.39  tff(c_8589, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdf_Alt))).
% 13.16/4.39  tff(c_8588, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdf_Bag))).
% 13.16/4.39  tff(c_8587, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdf_XMLLiteral))).
% 13.16/4.39  tff(c_8586, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdfs_Seq))).
% 13.16/4.39  tff(c_4884, plain, (![D_24, C_285]: (icext(D_24, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subClassOf, C_285, D_24) | ~iext(uri_rdfs_range, uri_skos_prefLabel, C_285)))).
% 13.16/4.39  tff(c_3875, plain, (![C_28, C_239]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_239) | ~iext(uri_rdfs_subClassOf, C_239, uri_rdf_Bag)))).
% 13.16/4.39  tff(c_8403, plain, (![D_11]: (~iext(uri_rdfs_range, uri_skos_altLabel, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.16/4.39  tff(c_8402, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdf_XMLLiteral))).
% 13.16/4.39  tff(c_8401, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdf_Alt))).
% 13.16/4.39  tff(c_8400, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdf_Bag))).
% 13.16/4.39  tff(c_8384, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdfs_Seq))).
% 13.16/4.39  tff(c_4773, plain, (![Q_32, P_278]: (iext(Q_32, P_278, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_278, uri_rdfs_isDefinedBy)))).
% 13.16/4.39  tff(c_4492, plain, (![D_24, C_271]: (icext(D_24, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subClassOf, C_271, D_24) | ~iext(uri_rdfs_range, uri_skos_altLabel, C_271)))).
% 13.16/4.39  tff(c_6169, plain, (![C_28, D_336]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_336) | ~icext(uri_rdfs_Datatype, D_336)))).
% 13.16/4.39  tff(c_6168, plain, (![Q_32, D_336]: (iext(Q_32, D_336, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_336)))).
% 13.16/4.39  tff(c_8181, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_first))).
% 13.16/4.39  tff(c_8180, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_object))).
% 13.16/4.39  tff(c_8179, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_subject))).
% 13.16/4.39  tff(c_8178, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_domain))).
% 13.16/4.39  tff(c_8177, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_rest))).
% 13.16/4.39  tff(c_8176, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_range))).
% 13.16/4.39  tff(c_8175, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_predicate))).
% 13.16/4.39  tff(c_5155, plain, (![C_13, Q_300]: (icext(C_13, uri_ex_foo) | ~iext(uri_rdfs_domain, Q_300, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, Q_300)))).
% 13.16/4.39  tff(c_8097, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_domain))).
% 13.16/4.39  tff(c_8096, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_first))).
% 13.16/4.39  tff(c_8095, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_subject))).
% 13.16/4.39  tff(c_8094, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_object))).
% 13.34/4.39  tff(c_8093, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_range))).
% 13.34/4.39  tff(c_8092, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_rest))).
% 13.34/4.39  tff(c_8091, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_predicate))).
% 13.34/4.39  tff(c_5247, plain, (![C_13, Q_307]: (icext(C_13, uri_ex_foo) | ~iext(uri_rdfs_domain, Q_307, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, Q_307)))).
% 13.34/4.39  tff(c_8013, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 13.34/4.39  tff(c_8012, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_label))).
% 13.34/4.39  tff(c_1288, plain, (![P_83, P_10]: (iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_83, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.34/4.39  tff(c_1444, plain, (![Q_86, D_11]: (iext(Q_86, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.34/4.39  tff(c_1443, plain, (![Q_86, P_10]: (iext(Q_86, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_86) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.34/4.39  tff(c_7954, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 13.34/4.39  tff(c_1263, plain, (![C_80, D_11]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.34/4.39  tff(c_1445, plain, (![Q_86, X_7, C_8]: (iext(Q_86, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86) | ~icext(C_8, X_7)))).
% 13.34/4.39  tff(c_7855, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 13.34/4.39  tff(c_7839, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 13.34/4.39  tff(c_1447, plain, (![Q_86, P_37]: (iext(Q_86, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_86) | ~ip(P_37)))).
% 13.34/4.39  tff(c_5584, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_5488, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_1446, plain, (![Q_86, P_6]: (iext(Q_86, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86) | ~ip(P_6)))).
% 13.34/4.39  tff(c_5631, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_5672, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_5489, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 13.34/4.39  tff(c_5520, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_5632, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 13.34/4.39  tff(c_7430, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))).
% 13.34/4.39  tff(c_5673, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 13.34/4.39  tff(c_5440, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.34/4.39  tff(c_5552, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 13.34/4.39  tff(c_1448, plain, (![Q_86, C_27]: (iext(Q_86, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86) | ~ic(C_27)))).
% 13.34/4.39  tff(c_5434, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))).
% 13.34/4.40  tff(c_5780, plain, (![C_72]: (icext(uri_rdfs_Class, C_72) | ~iext(uri_rdfs_range, uri_skos_altLabel, C_72)))).
% 13.34/4.40  tff(c_5779, plain, (![C_72]: (icext(uri_rdfs_Class, C_72) | ~iext(uri_rdfs_range, uri_skos_prefLabel, C_72)))).
% 13.34/4.40  tff(c_5585, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdf_Bag)))).
% 13.34/4.40  tff(c_5443, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.34/4.40  tff(c_5644, plain, (![C_332, X_333]: (icext(uri_rdfs_Class, C_332) | ~icext(C_332, X_333)))).
% 13.34/4.40  tff(c_5465, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_946, 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)))).
% 13.34/4.40  tff(c_5462, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_5459, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_5456, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_5453, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_5450, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 13.34/4.40  tff(c_1265, plain, (![C_80, C_9]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, C_9) | ~ic(C_9)))).
% 13.34/4.40  tff(c_1449, plain, (![Q_86, C_9]: (iext(Q_86, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86) | ~ic(C_9)))).
% 13.34/4.40  tff(c_5367, plain, (![D_325]: (icext(uri_rdfs_Class, D_325) | ~icext(uri_rdfs_Datatype, D_325)))).
% 13.34/4.40  tff(c_1170, 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)))).
% 13.34/4.40  tff(c_5337, plain, (![P_322]: (icext(uri_rdf_Property, P_322) | ~icext(uri_rdfs_ContainerMembershipProperty, P_322)))).
% 13.34/4.40  tff(c_1169, 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)))).
% 13.34/4.40  tff(c_1669, plain, (![D_24, P_92]: (icext(D_24, P_92) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_92)))).
% 13.34/4.40  tff(c_1171, 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)))).
% 13.34/4.40  tff(c_1172, plain, (![C_76, P_6]: (icext(C_76, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76) | ~ip(P_6)))).
% 13.34/4.40  tff(c_791, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))).
% 13.34/4.40  tff(c_949, plain, (![C_72, C_27]: (icext(C_72, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72) | ~ic(C_27)))).
% 13.34/4.40  tff(c_5261, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdf_type))).
% 13.34/4.40  tff(c_1174, plain, (![C_76, C_27]: (icext(C_76, C_27) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76) | ~ic(C_27)))).
% 13.34/4.40  tff(c_5256, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_subPropertyOf))).
% 13.34/4.40  tff(c_5255, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_subClassOf))).
% 13.34/4.40  tff(c_5207, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_1450, plain, (![Q_86]: (iext(Q_86, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, Q_86)))).
% 13.34/4.40  tff(c_792, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))).
% 13.34/4.40  tff(c_5177, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_propertyDisjointWith, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_948, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))).
% 13.34/4.40  tff(c_5172, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdf_type))).
% 13.34/4.40  tff(c_5171, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_1173, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))).
% 13.34/4.40  tff(c_5166, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_5164, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_subPropertyOf))).
% 13.34/4.40  tff(c_5163, plain, (~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_subClassOf))).
% 13.34/4.40  tff(c_1451, plain, (![Q_86]: (iext(Q_86, uri_ex_foo, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, Q_86)))).
% 13.34/4.40  tff(c_5115, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_5108, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 13.34/4.40  tff(c_5087, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 13.34/4.40  tff(c_1491, plain, (![Q_86]: (iext(Q_86, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_1474, plain, (![Q_86]: (iext(Q_86, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1462, plain, (![Q_86]: (iext(Q_86, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_1486, plain, (![Q_86]: (iext(Q_86, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.40  tff(c_1457, plain, (![Q_86]: (iext(Q_86, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.40  tff(c_1452, plain, (![Q_86]: (iext(Q_86, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1480, plain, (![Q_86]: (iext(Q_86, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1504, plain, (![Q_86]: (iext(Q_86, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_1498, plain, (![Q_86]: (iext(Q_86, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_1455, plain, (![Q_86]: (iext(Q_86, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_1483, plain, (![Q_86]: (iext(Q_86, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_4906, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdf_Property))).
% 13.34/4.40  tff(c_1492, plain, (![Q_86]: (iext(Q_86, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_4905, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdfs_Datatype))).
% 13.34/4.40  tff(c_4904, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdfs_Class))).
% 13.34/4.40  tff(c_4903, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdfs_Literal))).
% 13.34/4.40  tff(c_4902, plain, (~iext(uri_rdfs_range, uri_skos_prefLabel, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.40  tff(c_1463, plain, (![Q_86]: (iext(Q_86, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_952, plain, (![C_72]: (icext(C_72, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, uri_skos_prefLabel, C_72)))).
% 13.34/4.40  tff(c_1476, plain, (![Q_86]: (iext(Q_86, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_1509, plain, (![Q_86]: (iext(Q_86, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1507, plain, (![Q_86]: (iext(Q_86, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_1266, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Seq)))).
% 13.34/4.40  tff(c_1467, plain, (![Q_86]: (iext(Q_86, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1271, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Datatype)))).
% 13.34/4.40  tff(c_1291, plain, (![P_83]: (iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_isDefinedBy)))).
% 13.34/4.40  tff(c_1499, plain, (![Q_86]: (iext(Q_86, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.40  tff(c_1490, plain, (![Q_86]: (iext(Q_86, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_86)))).
% 13.34/4.40  tff(c_1503, plain, (![Q_86]: (iext(Q_86, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_1501, plain, (![Q_86]: (iext(Q_86, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_1460, plain, (![Q_86]: (iext(Q_86, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.40  tff(c_4511, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 13.34/4.40  tff(c_4510, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdfs_Class))).
% 13.34/4.40  tff(c_4509, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdfs_Literal))).
% 13.34/4.40  tff(c_4497, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdfs_Datatype))).
% 13.34/4.40  tff(c_1458, plain, (![Q_86]: (iext(Q_86, uri_skos_altLabel, uri_owl_AnnotationProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.40  tff(c_4496, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdf_Property))).
% 13.34/4.40  tff(c_4495, plain, (~iext(uri_rdfs_range, uri_skos_altLabel, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.40  tff(c_951, plain, (![C_72]: (icext(C_72, literal_plain(dat_str_foo)) | ~iext(uri_rdfs_range, uri_skos_altLabel, C_72)))).
% 13.34/4.41  tff(c_4465, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_1514, plain, (![Q_86]: (iext(Q_86, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_4453, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_1496, plain, (![Q_86]: (iext(Q_86, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.41  tff(c_1506, plain, (![Q_86]: (iext(Q_86, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_4430, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_4429, plain, (~iext(uri_rdfs_subClassOf, uri_owl_AnnotationProperty, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_4417, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_1456, plain, (![Q_86]: (iext(Q_86, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.41  tff(c_4416, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 13.34/4.41  tff(c_1479, plain, (![Q_86]: (iext(Q_86, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_1267, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))).
% 13.34/4.41  tff(c_1494, plain, (![Q_86]: (iext(Q_86, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1478, plain, (![Q_86]: (iext(Q_86, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_1461, plain, (![Q_86]: (iext(Q_86, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_4119, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_propertyDisjointWith))).
% 13.34/4.41  tff(c_1471, plain, (![Q_86]: (iext(Q_86, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1465, plain, (![Q_86]: (iext(Q_86, uri_skos_prefLabel, uri_skos_altLabel) | ~iext(uri_rdfs_subPropertyOf, uri_owl_propertyDisjointWith, Q_86)))).
% 13.34/4.41  tff(c_1512, plain, (![Q_86]: (iext(Q_86, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_1482, plain, (![Q_86]: (iext(Q_86, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1290, plain, (![P_83]: (iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_label) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_skos_prefLabel)))).
% 13.34/4.41  tff(c_1511, plain, (![Q_86]: (iext(Q_86, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1500, plain, (![Q_86]: (iext(Q_86, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1477, plain, (![Q_86]: (iext(Q_86, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1495, plain, (![Q_86]: (iext(Q_86, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1473, plain, (![Q_86]: (iext(Q_86, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1508, plain, (![Q_86]: (iext(Q_86, uri_skos_prefLabel, uri_owl_AnnotationProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_1464, plain, (![Q_86]: (iext(Q_86, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1515, plain, (![Q_86]: (iext(Q_86, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.41  tff(c_1469, plain, (![Q_86]: (iext(Q_86, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1488, plain, (![Q_86]: (iext(Q_86, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1497, plain, (![Q_86]: (iext(Q_86, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1475, plain, (![Q_86]: (iext(Q_86, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1468, plain, (![Q_86]: (iext(Q_86, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_3934, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 13.34/4.41  tff(c_3922, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 13.34/4.41  tff(c_1487, plain, (![Q_86]: (iext(Q_86, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_3910, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 13.34/4.41  tff(c_1453, plain, (![Q_86]: (iext(Q_86, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_3909, plain, (~iext(uri_rdfs_subClassOf, uri_owl_AnnotationProperty, uri_rdf_Bag))).
% 13.34/4.41  tff(c_3897, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 13.34/4.41  tff(c_1484, plain, (![Q_86]: (iext(Q_86, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_3896, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 13.34/4.41  tff(c_1489, plain, (![Q_86]: (iext(Q_86, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_86)))).
% 13.34/4.41  tff(c_3884, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 13.34/4.41  tff(c_3883, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 13.34/4.41  tff(c_1269, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 13.34/4.41  tff(c_3641, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 13.34/4.41  tff(c_1481, plain, (![Q_86]: (iext(Q_86, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_3629, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 13.34/4.41  tff(c_3617, plain, (~iext(uri_rdfs_subClassOf, uri_owl_AnnotationProperty, uri_rdf_Alt))).
% 13.34/4.41  tff(c_1493, plain, (![Q_86]: (iext(Q_86, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_3616, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 13.34/4.41  tff(c_1292, plain, (![P_83]: (iext(uri_rdfs_subPropertyOf, P_83, uri_rdfs_label) | ~iext(uri_rdfs_subPropertyOf, P_83, uri_skos_altLabel)))).
% 13.34/4.41  tff(c_1472, plain, (![Q_86]: (iext(Q_86, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1510, plain, (![Q_86]: (iext(Q_86, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_3585, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 13.34/4.41  tff(c_3584, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 13.34/4.41  tff(c_3575, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 13.34/4.41  tff(c_1270, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_ContainerMembershipProperty)))).
% 13.34/4.41  tff(c_3574, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 13.34/4.41  tff(c_1466, plain, (![Q_86]: (iext(Q_86, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_86)))).
% 13.34/4.41  tff(c_1268, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 13.34/4.41  tff(c_1505, plain, (![Q_86]: (iext(Q_86, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_1768, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1817, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1912, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1866, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1702, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1953, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1754, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1502, plain, (![Q_86]: (iext(Q_86, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_2080, plain, (![D_24]: (icext(D_24, uri_skos_altLabel) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1879, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1842, plain, (![D_24]: (icext(D_24, uri_owl_AnnotationProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1716, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1980, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1804, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_1729, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_3019, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 13.34/4.41  tff(c_1485, plain, (![Q_86]: (iext(Q_86, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_86)))).
% 13.34/4.41  tff(c_1781, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1893, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1930, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_2048, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_2023, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_2100, plain, (![D_24]: (icext(D_24, uri_skos_prefLabel) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_2258, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_2142, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_2061, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1454, plain, (![Q_86]: (iext(Q_86, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.41  tff(c_2129, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.41  tff(c_2247, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_2776, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 13.34/4.41  tff(c_1543, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.41  tff(c_1575, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.34/4.41  tff(c_1566, plain, (![D_24]: (icext(D_24, uri_skos_prefLabel) | ~iext(uri_rdfs_subClassOf, uri_owl_AnnotationProperty, D_24)))).
% 13.34/4.41  tff(c_1557, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.34/4.42  tff(c_1470, plain, (![Q_86]: (iext(Q_86, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_86)))).
% 13.34/4.42  tff(c_2674, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 13.34/4.42  tff(c_2673, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 13.34/4.42  tff(c_2652, plain, (~icext(uri_rdfs_Datatype, uri_owl_AnnotationProperty))).
% 13.34/4.42  tff(c_1590, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 13.34/4.42  tff(c_1569, plain, (![D_24]: (icext(D_24, uri_skos_altLabel) | ~iext(uri_rdfs_subClassOf, uri_owl_AnnotationProperty, D_24)))).
% 13.34/4.42  tff(c_2620, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.42  tff(c_1459, plain, (![Q_86]: (iext(Q_86, uri_skos_prefLabel, uri_rdfs_label) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_86)))).
% 13.34/4.42  tff(c_1563, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 13.34/4.42  tff(c_1546, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_2574, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 13.34/4.42  tff(c_1552, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 13.34/4.42  tff(c_1584, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_1537, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_1587, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_1513, plain, (![Q_86]: (iext(Q_86, uri_skos_altLabel, uri_rdfs_label) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_86)))).
% 13.34/4.42  tff(c_1560, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_1578, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_2442, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 13.34/4.42  tff(c_1572, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 13.34/4.42  tff(c_1581, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_2396, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 13.34/4.42  tff(c_1540, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 13.34/4.42  tff(c_1195, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_979, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.42  tff(c_969, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 13.34/4.42  tff(c_2357, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 13.34/4.42  tff(c_793, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))).
% 13.34/4.42  tff(c_1191, plain, (![C_76]: (icext(C_76, uri_skos_prefLabel) | ~iext(uri_rdfs_domain, uri_owl_propertyDisjointWith, C_76)))).
% 13.34/4.42  tff(c_1203, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1199, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1190, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_991, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))).
% 13.34/4.42  tff(c_1240, plain, (![C_76]: (icext(C_76, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1241, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.42  tff(c_1230, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1231, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1201, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1198, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_960, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_72)))).
% 13.34/4.42  tff(c_1228, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1221, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_2252, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 13.34/4.42  tff(c_1183, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.42  tff(c_2246, plain, (ip(uri_rdfs_comment))).
% 13.34/4.42  tff(c_2240, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 13.34/4.42  tff(c_1196, plain, (![C_76]: (icext(C_76, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1205, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1219, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1180, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_995, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 13.34/4.42  tff(c_1223, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1004, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 13.34/4.42  tff(c_1181, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1176, plain, (![C_76]: (icext(C_76, uri_ex_foo) | ~iext(uri_rdfs_domain, uri_skos_altLabel, C_76)))).
% 13.34/4.42  tff(c_1202, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1200, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1179, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1224, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1226, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1206, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1238, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1194, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_2136, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 13.34/4.42  tff(c_964, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.42  tff(c_2123, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 13.34/4.42  tff(c_1182, plain, (![C_76]: (icext(C_76, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.42  tff(c_1209, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1178, plain, (![C_76]: (icext(C_76, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1189, plain, (![C_76]: (icext(C_76, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_2092, plain, (icext(uri_rdf_Property, uri_skos_prefLabel))).
% 13.34/4.42  tff(c_1185, plain, (![C_76]: (icext(C_76, uri_skos_prefLabel) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76)))).
% 13.34/4.42  tff(c_970, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 13.34/4.42  tff(c_1177, plain, (![C_76]: (icext(C_76, uri_ex_foo) | ~iext(uri_rdfs_domain, uri_skos_prefLabel, C_76)))).
% 13.34/4.42  tff(c_2072, plain, (icext(uri_rdf_Property, uri_skos_altLabel))).
% 13.34/4.42  tff(c_1239, plain, (![C_76]: (icext(C_76, uri_skos_altLabel) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76)))).
% 13.34/4.42  tff(c_1235, plain, (![C_76]: (icext(C_76, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_2053, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 13.34/4.42  tff(c_1217, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_2040, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 13.34/4.42  tff(c_1188, plain, (![C_76]: (icext(C_76, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1197, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1204, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_2015, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 13.34/4.42  tff(c_1207, plain, (![C_76]: (icext(C_76, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1210, plain, (![C_76]: (icext(C_76, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1236, plain, (![C_76]: (icext(C_76, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_986, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 13.34/4.42  tff(c_1193, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1208, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1972, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 13.34/4.42  tff(c_1211, plain, (![C_76]: (icext(C_76, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1218, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1234, plain, (![C_76]: (icext(C_76, uri_skos_prefLabel) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1947, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 13.34/4.42  tff(c_1215, plain, (![C_76]: (icext(C_76, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.42  tff(c_1233, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1225, plain, (![C_76]: (icext(C_76, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1929, plain, (ip(uri_rdf_predicate))).
% 13.34/4.42  tff(c_1923, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 13.34/4.42  tff(c_1237, plain, (![C_76]: (icext(C_76, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_977, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 13.34/4.42  tff(c_1904, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 13.34/4.42  tff(c_1216, plain, (![C_76]: (icext(C_76, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_76)))).
% 13.34/4.42  tff(c_997, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 13.34/4.42  tff(c_1885, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 13.34/4.42  tff(c_1220, plain, (![C_76]: (icext(C_76, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.42  tff(c_1880, plain, (ic(uri_rdf_List))).
% 13.34/4.42  tff(c_1873, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 13.34/4.42  tff(c_1015, plain, (![C_72]: (icext(C_72, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.42  tff(c_1860, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 13.34/4.42  tff(c_987, plain, (![C_72]: (icext(C_72, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 13.34/4.42  tff(c_1227, plain, (![C_76]: (icext(C_76, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_1213, plain, (![C_76]: (icext(C_76, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.42  tff(c_1843, plain, (ic(uri_owl_AnnotationProperty))).
% 13.34/4.42  tff(c_1836, plain, (icext(uri_rdfs_Class, uri_owl_AnnotationProperty))).
% 13.34/4.42  tff(c_1009, plain, (![C_72]: (icext(C_72, uri_owl_AnnotationProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.42  tff(c_1184, plain, (![C_76]: (icext(C_76, uri_skos_altLabel) | ~iext(uri_rdfs_domain, uri_rdf_type, C_76)))).
% 13.34/4.42  tff(c_963, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 13.34/4.42  tff(c_1811, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 13.34/4.42  tff(c_1016, plain, (![C_72]: (icext(C_72, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 13.34/4.42  tff(c_1798, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 13.34/4.42  tff(c_1212, plain, (![C_76]: (icext(C_76, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.43  tff(c_962, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.43  tff(c_1186, plain, (![C_76]: (icext(C_76, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.43  tff(c_1773, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 13.34/4.43  tff(c_1214, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_76)))).
% 13.34/4.43  tff(c_1760, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 13.34/4.43  tff(c_1229, plain, (![C_76]: (icext(C_76, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_76)))).
% 13.34/4.43  tff(c_1755, plain, (ic(uri_rdfs_Statement))).
% 13.34/4.43  tff(c_1748, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 13.34/4.43  tff(c_1000, plain, (![C_72]: (icext(C_72, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 13.34/4.43  tff(c_984, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_72)))).
% 13.34/4.43  tff(c_1222, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_76)))).
% 13.34/4.43  tff(c_1723, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_961, plain, (![C_72]: (icext(C_72, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_72)))).
% 13.34/4.43  tff(c_1710, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.43  tff(c_1002, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_72)))).
% 13.34/4.43  tff(c_966, plain, (![C_72]: (icext(C_72, uri_skos_altLabel) | ~iext(uri_rdfs_range, uri_owl_propertyDisjointWith, C_72)))).
% 13.34/4.43  tff(c_1696, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 13.34/4.43  tff(c_958, plain, (![C_72]: (icext(C_72, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_72)))).
% 13.34/4.43  tff(c_1691, plain, (ip(uri_rdfs_member))).
% 13.34/4.43  tff(c_776, plain, (![P_68]: (ip(P_68) | ~icext(uri_rdfs_ContainerMembershipProperty, P_68)))).
% 13.34/4.43  tff(c_725, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 13.34/4.43  tff(c_757, plain, (![D_67]: (ic(D_67) | ~icext(uri_rdfs_Datatype, D_67)))).
% 13.34/4.43  tff(c_661, plain, (![X_63]: (ip(X_63) | ~icext(uri_rdf_Property, X_63)))).
% 13.34/4.43  tff(c_1607, plain, (ic(uri_rdfs_Resource))).
% 13.34/4.43  tff(c_742, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 13.34/4.43  tff(c_731, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 13.34/4.43  tff(c_740, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 13.34/4.43  tff(c_736, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 13.34/4.43  tff(c_735, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 13.34/4.43  tff(c_732, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 13.34/4.43  tff(c_729, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 13.34/4.43  tff(c_727, plain, (icext(uri_owl_AnnotationProperty, uri_skos_altLabel))).
% 13.34/4.43  tff(c_739, plain, (icext(uri_owl_AnnotationProperty, uri_skos_prefLabel))).
% 13.34/4.43  tff(c_726, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 13.34/4.43  tff(c_730, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 13.34/4.43  tff(c_737, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 13.34/4.43  tff(c_733, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 13.34/4.43  tff(c_734, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 13.34/4.43  tff(c_741, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 13.34/4.43  tff(c_738, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 13.34/4.43  tff(c_728, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 13.34/4.43  tff(c_648, plain, (ic(uri_rdf_XMLLiteral))).
% 13.34/4.43  tff(c_566, plain, (ip(uri_rdf__1))).
% 13.34/4.43  tff(c_568, plain, (ip(uri_rdf_object))).
% 13.34/4.43  tff(c_569, plain, (ip(uri_rdf_value))).
% 13.34/4.43  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.34/4.43  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.34/4.43  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.34/4.43  tff(c_567, plain, (ip(uri_rdf__3))).
% 13.34/4.43  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.34/4.43  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.34/4.43  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.34/4.43  tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 13.34/4.43  tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 13.34/4.43  tff(c_647, plain, (ic(uri_rdfs_Seq))).
% 13.34/4.43  tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 13.34/4.43  tff(c_480, plain, (ip(uri_rdfs_subPropertyOf))).
% 13.34/4.43  tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 13.34/4.43  tff(c_649, plain, (ic(uri_rdf_Alt))).
% 13.34/4.43  tff(c_650, plain, (ic(uri_rdf_Bag))).
% 13.34/4.43  tff(c_651, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.43  tff(c_652, plain, (ic(uri_rdfs_Datatype))).
% 13.34/4.43  tff(c_439, plain, (ip(uri_rdfs_range))).
% 13.34/4.43  tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 13.34/4.43  tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 13.34/4.43  tff(c_432, plain, (ip(uri_owl_propertyDisjointWith))).
% 13.34/4.43  tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 13.34/4.43  tff(c_587, plain, (ip(uri_rdfs_seeAlso))).
% 13.34/4.43  tff(c_588, plain, (ip(uri_rdfs_label))).
% 13.34/4.43  tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 13.34/4.43  tff(c_572, plain, (ip(uri_rdf_subject))).
% 13.34/4.43  tff(c_573, plain, (ip(uri_rdf__2))).
% 13.34/4.43  tff(c_574, plain, (ip(uri_rdf_rest))).
% 13.34/4.43  tff(c_575, plain, (ip(uri_rdf_first))).
% 13.34/4.43  tff(c_453, plain, (ip(uri_rdfs_subClassOf))).
% 13.34/4.43  tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 13.34/4.43  tff(c_533, plain, (ip(uri_skos_prefLabel))).
% 13.34/4.43  tff(c_534, plain, (ip(uri_rdfs_isDefinedBy))).
% 13.34/4.43  tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 13.34/4.43  tff(c_507, plain, (ic(uri_rdfs_Literal))).
% 13.34/4.43  tff(c_508, plain, (ic(uri_rdfs_Container))).
% 13.34/4.43  tff(c_436, plain, (ip(uri_rdfs_domain))).
% 13.34/4.43  tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 13.34/4.43  tff(c_510, plain, (ic(uri_rdf_Property))).
% 13.34/4.43  tff(c_511, plain, (ic(uri_rdfs_Class))).
% 13.34/4.43  tff(c_445, plain, (ip(uri_rdf_type))).
% 13.34/4.43  tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 13.34/4.43  tff(c_417, plain, (ip(uri_skos_altLabel))).
% 13.34/4.43  tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 13.34/4.43  tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 13.34/4.43  tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 13.34/4.43  tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 13.34/4.43  tff(c_180, plain, (iext(uri_skos_altLabel, uri_ex_foo, literal_plain(dat_str_foo)))).
% 13.34/4.43  tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 13.34/4.43  tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 13.34/4.43  tff(c_182, plain, (iext(uri_skos_prefLabel, uri_ex_foo, literal_plain(dat_str_foo)))).
% 13.34/4.43  tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.43  tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 13.34/4.43  tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 13.34/4.43  tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 13.34/4.43  tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 13.34/4.43  tff(c_188, plain, (iext(uri_rdf_type, uri_skos_altLabel, uri_owl_AnnotationProperty))).
% 13.34/4.43  tff(c_190, plain, (iext(uri_rdfs_subPropertyOf, uri_skos_prefLabel, uri_rdfs_label))).
% 13.34/4.43  tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 13.34/4.43  tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 13.34/4.43  tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 13.34/4.43  tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_184, plain, (iext(uri_owl_propertyDisjointWith, uri_skos_prefLabel, uri_skos_altLabel))).
% 13.34/4.43  tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 13.34/4.43  tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 13.34/4.43  tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 13.34/4.43  tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 13.34/4.43  tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 13.34/4.43  tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 13.34/4.43  tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.43  tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 13.34/4.43  tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 13.34/4.43  tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 13.34/4.43  tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 13.34/4.43  tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 13.34/4.43  tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 13.34/4.43  tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 13.34/4.43  tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 13.34/4.43  tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 13.34/4.43  tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 13.34/4.43  tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 13.34/4.43  tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 13.34/4.43  tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 13.34/4.43  tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 13.34/4.43  tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 13.34/4.43  tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 13.34/4.43  tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 13.34/4.43  tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 13.34/4.43  tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 13.34/4.43  tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 13.34/4.43  tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 13.34/4.44  tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 13.34/4.44  tff(c_192, plain, (iext(uri_rdf_type, uri_skos_prefLabel, uri_owl_AnnotationProperty))).
% 13.34/4.44  tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 13.34/4.44  tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 13.34/4.44  tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 13.34/4.44  tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 13.34/4.44  tff(c_186, plain, (iext(uri_rdfs_subPropertyOf, uri_skos_altLabel, uri_rdfs_label))).
% 13.34/4.44  tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 13.34/4.44  tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 13.34/4.44  tff(c_198, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 13.34/4.44  tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 13.34/4.44  % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.34/4.44  
%------------------------------------------------------------------------------