Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SWB015-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %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  : 600s
% DateTime : Tue Jul 19 19:15:22 EDT 2022

% Result   : Satisfiable 0.78s 0.96s
% Output   : Saturation 0.83s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13  % Problem  : SWB015-10 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.35  % Computer : n018.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 600
% 0.13/0.35  % DateTime : Wed Jun  1 05:33:29 EDT 2022
% 0.13/0.35  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.78/0.96  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.96  
% 0.78/0.96  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.78/0.96  |- ifeq $A $A $B $C = $B
% 0.78/0.96  |- ifeq (iext $P $S $O) true (ip $P) true = true
% 0.78/0.96  |- ir $X = true
% 0.78/0.96  |- ifeq (lv $X) true true true = true
% 0.78/0.96  |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true
% 0.78/0.96  |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true
% 0.78/0.96  |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true
% 0.78/0.97  |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true
% 0.78/0.97  |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.78/0.97  |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true
% 0.78/0.97  |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true
% 0.78/0.97  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true =
% 0.78/0.97     true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true
% 0.78/0.97  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true
% 0.78/0.97       (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.78/0.97       uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true
% 0.78/0.97  |- ifeq (icext uri_rdfs_Datatype $D) true
% 0.78/0.97       (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_domain $P $C) true
% 0.78/0.97       (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true
% 0.78/0.97  |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true
% 0.78/0.97  |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true
% 0.78/0.97  |- icext uri_rdfs_Resource $X = true
% 0.78/0.97  |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true
% 0.78/0.97  |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true
% 0.78/0.97  |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_range $P $C) true
% 0.78/0.97       (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.78/0.97  |- ifeq (icext $C $X) true
% 0.78/0.97       (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true =
% 0.78/0.97     true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.78/0.97  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subClassOf $D $E) true
% 0.78/0.97       (ifeq (iext uri_rdfs_subClassOf $C $D) true
% 0.78/0.97          (iext uri_rdfs_subClassOf $C $E) true) true = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.78/0.97       (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.78/0.97  |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true
% 0.78/0.97  |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true
% 0.78/0.97       (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.78/0.97          (iext uri_rdfs_subPropertyOf $P $R) true) true = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true
% 0.78/0.97  |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true
% 0.78/0.97  |- ~(iext uri_owl_sameAs uri_owl_sameAs uri_owl_sameAs = true)
% 0.78/0.97  |- ip uri_rdf__1 = true
% 0.78/0.97  |- ip uri_rdf__2 = true
% 0.78/0.97  |- ip uri_rdf__3 = true
% 0.78/0.97  |- ip uri_rdf_first = true
% 0.78/0.97  |- ip uri_rdf_object = true
% 0.78/0.97  |- ip uri_rdf_rest = true
% 0.78/0.97  |- ip uri_rdf_subject = true
% 0.78/0.97  |- ip uri_rdf_type = true
% 0.78/0.97  |- ip uri_rdf_value = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true
% 0.78/0.97  |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true
% 0.78/0.97  |- ic uri_rdfs_Container = true
% 0.78/0.97  |- ic uri_rdfs_Literal = true
% 0.78/0.97  |- ic uri_rdf_Property = true
% 0.78/0.97  |- ic uri_rdfs_Class = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true
% 0.78/0.97  |- icext uri_rdfs_Class uri_rdfs_Container = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true
% 0.78/0.97  |- icext uri_rdfs_Class uri_rdfs_Literal = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true
% 0.78/0.97  |- icext uri_rdfs_Class uri_rdf_Property = true
% 0.78/0.97  |- ic uri_rdfs_Resource = true
% 0.78/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true
% 0.83/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true
% 0.83/0.97  |- icext uri_rdfs_Class uri_rdfs_Class = true
% 0.83/0.97  |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true
% 0.83/0.97  |- icext uri_rdfs_Class uri_rdfs_Resource = true
% 0.83/0.97  |- ic uri_rdf_Alt = true
% 0.83/0.97  |- ic uri_rdf_Bag = true
% 0.83/0.97  |- ic uri_rdf_XMLLiteral = true
% 0.83/0.97  |- ic uri_rdfs_ContainerMembershipProperty = true
% 0.83/0.97  |- ic uri_rdfs_Datatype = true
% 0.83/0.98  |- ic uri_rdfs_Seq = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdf_Alt = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdf_Bag = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.83/0.98       uri_rdfs_ContainerMembershipProperty = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.83/0.98       uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdfs_Seq = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true
% 0.83/0.98  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Class uri_rdfs_Datatype = true
% 0.83/0.98  |- ip uri_rdfs_seeAlso = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true
% 0.83/0.98  |- ip uri_rdfs_isDefinedBy = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy =
% 0.83/0.98     true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class =
% 0.83/0.98     true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true
% 0.83/0.98  |- iext uri_rdf_type $_55 uri_rdfs_Resource = true
% 0.83/0.98  |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf__1 = true
% 0.83/0.98  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf__2 = true
% 0.83/0.98  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf__3 = true
% 0.83/0.98  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_first = true
% 0.83/0.98  |- icext uri_rdf_List uri_rdf_nil = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_object = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_rest = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_subject = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_type = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdf_value = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_seeAlso = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true
% 0.83/0.98  |- ip uri_rdfs_member = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_member = true
% 0.83/0.98  |- ifeq (iext uri_rdf__1 $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf__2 $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf__3 $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_first $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_object $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_rest $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_subject $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_type $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdf_value $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_isDefinedBy $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_member $_78 $_76) true true true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_seeAlso $_78 $_76) true true true = true
% 0.83/0.98  |- ip uri_rdfs_domain = true
% 0.83/0.98  |- ip uri_rdfs_range = true
% 0.83/0.98  |- ip uri_rdfs_subClassOf = true
% 0.83/0.98  |- ip uri_rdfs_subPropertyOf = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_domain $S $O) true true true = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_range $S $O) true true true = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf =
% 0.83/0.98     true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true
% 0.83/0.98  |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.83/0.98       uri_rdfs_subPropertyOf = true
% 0.83/0.98  |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_domain = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_subClassOf = true
% 0.83/0.98  |- icext uri_rdf_Property uri_rdfs_range = true
% 0.83/0.98  |- ifeq (icext $_111 $_113) true true true = true
% 0.83/0.98  |- ifeq (icext uri_rdf_Alt $_113) true (icext uri_rdf_Alt $_113) true =
% 0.83/0.98     true
% 0.83/0.98  |- ifeq (icext uri_rdf_Alt $_113) true (icext uri_rdfs_Container $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdf_Bag $_113) true (icext uri_rdf_Bag $_113) true =
% 0.83/0.98     true
% 0.83/0.98  |- ifeq (icext uri_rdf_Bag $_113) true (icext uri_rdfs_Container $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdf_Property $_113) true (icext uri_rdf_Property $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdf_XMLLiteral $_113) true
% 0.83/0.98       (icext uri_rdf_XMLLiteral $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdf_XMLLiteral $_113) true
% 0.83/0.98       (icext uri_rdfs_Literal $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Class $_113) true (icext uri_rdfs_Class $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Container $_113) true
% 0.83/0.98       (icext uri_rdfs_Container $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_113) true
% 0.83/0.98       (icext uri_rdf_Property $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_113) true
% 0.83/0.98       (icext uri_rdfs_ContainerMembershipProperty $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Datatype $_113) true (icext uri_rdfs_Class $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Datatype $_113) true
% 0.83/0.98       (icext uri_rdfs_Datatype $_113) true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Literal $_113) true (icext uri_rdfs_Literal $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Seq $_113) true (icext uri_rdfs_Container $_113)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (icext uri_rdfs_Seq $_113) true (icext uri_rdfs_Seq $_113) true =
% 0.83/0.98     true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_nil) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf__1) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf__2) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf__3) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_first) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_object) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_rest) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_subject) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_type) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_value) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_domain) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_isDefinedBy) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_member) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_range) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_seeAlso) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_subClassOf) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_subPropertyOf) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_Alt) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_Bag) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_Property) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_XMLLiteral) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Class) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Container) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Datatype) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Literal) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Resource) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_112) true
% 0.83/0.98       (icext $_112 uri_rdfs_Seq) true = true
% 0.83/0.98  |- ifeq
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_112)
% 0.83/0.98       true (icext $_112 uri_rdf__1) true = true
% 0.83/0.98  |- ifeq
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_112)
% 0.83/0.98       true (icext $_112 uri_rdf__2) true = true
% 0.83/0.98  |- ifeq
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_112)
% 0.83/0.98       true (icext $_112 uri_rdf__3) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_112) true
% 0.83/0.98       (icext $_112 uri_rdf_XMLLiteral) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_112) true
% 0.83/0.98       (icext $_112 $_113) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_Alt $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_Alt $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_Bag $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_Bag $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_Property $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Class $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Container $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_166)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_166)
% 0.83/0.98       true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Literal $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_166) true
% 0.83/0.98       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_166) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_Alt) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Container) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_Alt) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_Bag) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Container) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_Bag) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_Property) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.98  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_XMLLiteral) true
% 0.83/0.98       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Literal) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdf_XMLLiteral) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Class) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Container) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_ContainerMembershipProperty)
% 0.83/0.99       true (iext uri_rdfs_subClassOf $_164 uri_rdf_Property) true = true
% 0.83/0.99  |- ifeq
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_ContainerMembershipProperty)
% 0.83/0.99       true (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Datatype) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Class) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Datatype) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Literal) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Seq) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Container) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_164 uri_rdfs_Seq) true
% 0.83/0.99       (iext uri_rdfs_subClassOf $_164 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_223) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf uri_rdf__1 $_223) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_223) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf uri_rdf__2 $_223) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_223) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf uri_rdf__3 $_223) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_223) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_223) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $_221 uri_rdf__1) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf $_221 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $_221 uri_rdf__2) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf $_221 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $_221 uri_rdf__3) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf $_221 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $_221 uri_rdfs_isDefinedBy) true
% 0.83/0.99       (iext uri_rdfs_subPropertyOf $_221 uri_rdfs_seeAlso) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_List) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_nil $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf__1 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf__2 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf__3 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_first $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_object $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_rest $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_subject $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_type $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_value $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_domain $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_isDefinedBy $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_member $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_range $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_seeAlso $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_subClassOf $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_subPropertyOf $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_Alt $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_Bag $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_Property $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_XMLLiteral $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Class $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Container $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_ContainerMembershipProperty $_269) true
% 0.83/0.99          true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Datatype $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Literal $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Resource $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Class) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdfs_Seq $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_ContainerMembershipProperty)
% 0.83/0.99       true (ifeq (iext $_267 uri_rdf__1 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_ContainerMembershipProperty)
% 0.83/0.99       true (ifeq (iext $_267 uri_rdf__2 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_ContainerMembershipProperty)
% 0.83/0.99       true (ifeq (iext $_267 uri_rdf__3 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Datatype) true
% 0.83/0.99       (ifeq (iext $_267 uri_rdf_XMLLiteral $_269) true true true) true =
% 0.83/0.99     true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_267 uri_rdfs_Resource) true
% 0.83/0.99       (ifeq (iext $_267 $_268 $_269) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdf_type $_266) true (icext $_266 $_268)
% 0.83/0.99       true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__1) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__2) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__3) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_first) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_object) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_predicate) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_rest) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_subject) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_type) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_value) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_comment) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_domain) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_isDefinedBy) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_label) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_range) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_seeAlso) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subClassOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subPropertyOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__1) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__2) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__3) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_first) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_predicate) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_rest) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_subject) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_type) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_value) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_comment) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_domain) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_isDefinedBy) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_label) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_range) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_seeAlso) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subClassOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subPropertyOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_Alt) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_Bag) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_Property) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_XMLLiteral) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Class) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Container) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Datatype) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Literal) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Resource) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_Seq) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__1) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__2) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf__3) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_first) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_object) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_rest) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_subject) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_type) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdf_value) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_domain) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_isDefinedBy) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_member) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_range) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_seeAlso) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subClassOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_266) true
% 0.83/0.99       (icext $_266 uri_rdfs_subPropertyOf) true = true
% 0.83/0.99  |- ifeq (iext uri_rdf_first $_268 $_269) true (icext uri_rdf_List $_268)
% 0.83/0.99       true = true
% 0.83/0.99  |- ifeq (iext uri_rdf_object $_268 $_269) true
% 0.83/0.99       (icext uri_rdfs_Statement $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdf_predicate $_268 $_269) true
% 0.83/0.99       (icext uri_rdfs_Statement $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdf_rest $_268 $_269) true (icext uri_rdf_List $_268)
% 0.83/0.99       true = true
% 0.83/0.99  |- ifeq (iext uri_rdf_subject $_268 $_269) true
% 0.83/0.99       (icext uri_rdfs_Statement $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_comment $_268 $_269) true true true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $_268 $_269) true
% 0.83/0.99       (icext uri_rdf_Property $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_label $_268 $_269) true true true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_range $_268 $_269) true
% 0.83/0.99       (icext uri_rdf_Property $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf $_268 $_269) true
% 0.83/0.99       (icext uri_rdfs_Class $_268) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $_268 $_269) true
% 0.83/0.99       (icext uri_rdf_Property $_268) true = true
% 0.83/0.99  |- icext uri_rdf_Property uri_rdf_predicate = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.83/0.99       (icext $D uri_rdf_predicate) true = true
% 0.83/0.99  |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true
% 0.83/0.99  |- ip uri_rdf_predicate = true
% 0.83/0.99  |- ifeq (iext uri_rdf_predicate $S $O) true true true = true
% 0.83/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.83/0.99       (icext $C uri_rdf_predicate) true = true
% 0.83/0.99  |- icext uri_rdf_Property uri_rdfs_comment = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.83/0.99       (icext $D uri_rdfs_comment) true = true
% 0.83/0.99  |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true
% 0.83/0.99  |- ip uri_rdfs_comment = true
% 0.83/0.99  |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.83/0.99       (icext $C uri_rdfs_comment) true = true
% 0.83/0.99  |- icext uri_rdf_Property uri_rdfs_label = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.83/0.99       (icext $D uri_rdfs_label) true = true
% 0.83/0.99  |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true
% 0.83/0.99  |- ip uri_rdfs_label = true
% 0.83/0.99  |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.83/0.99       (icext $C uri_rdfs_label) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_List) true
% 0.83/0.99       (ifeq (iext $_437 $_438 uri_rdf_nil) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_437 $_438 uri_rdf__1) true true true) true = true
% 0.83/0.99  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/0.99       (ifeq (iext $_437 $_438 uri_rdf__2) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf__3) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_first) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_object) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_predicate) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_rest) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_subject) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_type) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_value) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_comment) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_domain) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_isDefinedBy) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_label) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_member) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_range) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_seeAlso) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_subClassOf) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdf_Property) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_subPropertyOf) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_Alt) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_Bag) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_Property) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_XMLLiteral) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Class) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Container) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_ContainerMembershipProperty) true
% 0.83/1.00          true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Datatype) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Literal) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Resource) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdfs_Seq) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00       true (ifeq (iext $_437 $_438 uri_rdf__1) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00       true (ifeq (iext $_437 $_438 uri_rdf__2) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00       true (ifeq (iext $_437 $_438 uri_rdf__3) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Datatype) true
% 0.83/1.00       (ifeq (iext $_437 $_438 uri_rdf_XMLLiteral) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_437 uri_rdfs_Resource) true
% 0.83/1.00       (ifeq (iext $_437 $_438 $_439) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Class) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Datatype) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Property) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_List) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdf_type $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_List) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Statement) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Property) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Class) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_List) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Class) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Literal) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Property) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Alt) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Container) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Bag) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_Property) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_XMLLiteral) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Literal) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Class) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Datatype) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_Seq) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf__1) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_member) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf__2) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf__3) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_first) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_object) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_predicate) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_rest) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_subject) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_type) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdf_value) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_comment) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_domain) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_isDefinedBy) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_seeAlso) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_label) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_range) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_subClassOf) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_436) true
% 0.83/1.00       (icext $_436 uri_rdfs_subPropertyOf) true = true
% 0.83/1.00  |- ifeq (iext uri_rdf_rest $_438 $_439) true (icext uri_rdf_List $_439)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdf_type $_438 $_439) true (icext uri_rdfs_Class $_439)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_comment $_438 $_439) true
% 0.83/1.00       (icext uri_rdfs_Literal $_439) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_domain $_438 $_439) true
% 0.83/1.00       (icext uri_rdfs_Class $_439) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_label $_438 $_439) true
% 0.83/1.00       (icext uri_rdfs_Literal $_439) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $_438 $_439) true (icext uri_rdfs_Class $_439)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf $_438 $_439) true
% 0.83/1.00       (icext uri_rdfs_Class $_439) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_438 $_439) true
% 0.83/1.00       (icext uri_rdf_Property $_439) true = true
% 0.83/1.00  |- icext uri_rdfs_Class uri_rdf_List = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $P $X uri_rdf_List) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $P uri_rdf_List $Y) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.83/1.00       (icext $D uri_rdf_List) true = true
% 0.83/1.00  |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true
% 0.83/1.00  |- ic uri_rdf_List = true
% 0.83/1.00  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true
% 0.83/1.00  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.83/1.00       (icext $C uri_rdf_List) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.83/1.00       (icext $C uri_rdf_List) true = true
% 0.83/1.00  |- ifeq (icext uri_rdf_List $X) true (icext uri_rdf_List $X) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true
% 0.83/1.00       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.83/1.00       (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true
% 0.83/1.00  |- icext uri_rdfs_Class uri_rdfs_Statement = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.83/1.00       (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.83/1.00       (icext $D uri_rdfs_Statement) true = true
% 0.83/1.00  |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true
% 0.83/1.00  |- ic uri_rdfs_Statement = true
% 0.83/1.00  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true
% 0.83/1.00  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.83/1.00       (icext $C uri_rdfs_Statement) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.83/1.00       (icext $C uri_rdfs_Statement) true = true
% 0.83/1.00  |- ifeq (icext uri_rdfs_Statement $X) true (icext uri_rdfs_Statement $X)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true
% 0.83/1.00       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.83/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_Alt uri_rdfs_Class) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_Bag uri_rdfs_Class) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_List uri_rdfs_Class) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_Property uri_rdfs_Class) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_XMLLiteral uri_rdfs_Class) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true
% 0.83/1.00          true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__1 uri_rdf_Property) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__1 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00          true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__2 uri_rdf_Property) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__2 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00          true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__3 uri_rdf_Property) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf__3 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.00          true true true) true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_first uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_nil uri_rdf_List) true true true) true =
% 0.83/1.00     true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_object uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_predicate uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_rest uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_subject uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_type uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdf_value uri_rdf_Property) true true true)
% 0.83/1.00       true = true
% 0.83/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.00       (ifeq (iext $_528 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.83/1.00       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Container uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.83/1.01          true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Literal uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Resource uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Seq uri_rdfs_Class) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Statement uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_comment uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_isDefinedBy uri_rdf_Property) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_label uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_member uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_range uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_seeAlso uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subClassOf uri_rdf_Property) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdf_type) true
% 0.83/1.01       (ifeq (iext $_528 $_530 uri_rdfs_Resource) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_first uri_rdf_List) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_object uri_rdfs_Statement) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_predicate uri_rdfs_Statement) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_subject uri_rdfs_Statement) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_type uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_comment uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_label uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_range uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_domain) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_first uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_predicate uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_subject uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_type uri_rdfs_Class) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_comment uri_rdfs_Literal) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_domain uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_label uri_rdfs_Literal) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_range uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_range) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Alt uri_rdf_Alt) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Alt uri_rdfs_Container) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Alt uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Bag uri_rdf_Bag) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Bag uri_rdfs_Container) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Bag uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_List uri_rdf_List) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_List uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Property uri_rdf_Property) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_Property uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_XMLLiteral uri_rdfs_Resource) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Class uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Container uri_rdfs_Container) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Container uri_rdfs_Resource) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq
% 0.83/1.01          (iext $_528 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.83/1.01          true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq
% 0.83/1.01          (iext $_528 uri_rdfs_ContainerMembershipProperty
% 0.83/1.01             uri_rdfs_ContainerMembershipProperty) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq
% 0.83/1.01          (iext $_528 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.83/1.01          true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Datatype uri_rdfs_Datatype) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Datatype uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Literal uri_rdfs_Literal) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Literal uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Resource uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Seq uri_rdfs_Container) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Seq uri_rdfs_Resource) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Seq uri_rdfs_Seq) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Statement uri_rdfs_Resource) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subClassOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_Statement uri_rdfs_Statement) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__1 uri_rdf__1) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__1 uri_rdfs_member) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__2 uri_rdf__2) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__2 uri_rdfs_member) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__3 uri_rdf__3) true true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf__3 uri_rdfs_member) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_first uri_rdf_first) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_object uri_rdf_object) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_predicate uri_rdf_predicate) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_rest uri_rdf_rest) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_subject uri_rdf_subject) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_type uri_rdf_type) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdf_value uri_rdf_value) true true true) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_comment uri_rdfs_comment) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_domain uri_rdfs_domain) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_label uri_rdfs_label) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_member uri_rdfs_member) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_range uri_rdfs_range) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true
% 0.83/1.01          true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_528 uri_rdfs_subPropertyOf) true
% 0.83/1.01       (ifeq (iext $_528 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true
% 0.83/1.01          true true) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_Alt uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_Bag uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_List uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_Property uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_XMLLiteral uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__1 uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__2 uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__3 uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true =
% 0.83/1.01     true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_first uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_nil uri_rdf_List) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_object uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_predicate uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_rest uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_subject uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_type uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdf_value uri_rdf_Property) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Container uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.83/1.01       true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Literal uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Resource uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Seq uri_rdfs_Class) true = true
% 0.83/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.01       (iext $_529 uri_rdfs_Statement uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_comment uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_domain uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_isDefinedBy uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_label uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_member uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_range uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_seeAlso uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subClassOf uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_529) true
% 0.83/1.02       (iext $_529 $_530 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_first uri_rdf_List) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_object uri_rdfs_Statement) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_predicate uri_rdfs_Statement) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_rest uri_rdf_List) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_subject uri_rdfs_Statement) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_type uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_value uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_comment uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_domain uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_label uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_range uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_first uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_predicate uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_rest uri_rdf_List) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_subject uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_type uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_value uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_comment uri_rdfs_Literal) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_domain uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_label uri_rdfs_Literal) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_range uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Alt uri_rdf_Alt) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Alt uri_rdfs_Container) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Alt uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Bag uri_rdf_Bag) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Bag uri_rdfs_Container) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Bag uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_List uri_rdf_List) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_List uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Property uri_rdf_Property) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_Property uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Class uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Container uri_rdfs_Container) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Container uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.83/1.02       true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_ContainerMembershipProperty
% 0.83/1.02          uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.83/1.02       true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Datatype uri_rdfs_Datatype) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Datatype uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Literal uri_rdfs_Literal) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Literal uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Resource uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Seq uri_rdfs_Container) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Seq uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Seq uri_rdfs_Seq) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Statement uri_rdfs_Resource) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_Statement uri_rdfs_Statement) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__1 uri_rdf__1) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__1 uri_rdfs_member) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__2 uri_rdf__2) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__2 uri_rdfs_member) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__3 uri_rdf__3) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf__3 uri_rdfs_member) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_first uri_rdf_first) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_object uri_rdf_object) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_predicate uri_rdf_predicate) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_rest uri_rdf_rest) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_subject uri_rdf_subject) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_type uri_rdf_type) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdf_value uri_rdf_value) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_comment uri_rdfs_comment) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_domain uri_rdfs_domain) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_label uri_rdfs_label) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_member uri_rdfs_member) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_range uri_rdfs_range) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_529) true
% 0.83/1.02       (iext $_529 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__1 $_530 $_531) true (iext uri_rdf__1 $_530 $_531)
% 0.83/1.02       true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__1 $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_member $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__2 $_530 $_531) true (iext uri_rdf__2 $_530 $_531)
% 0.83/1.02       true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__2 $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_member $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__3 $_530 $_531) true (iext uri_rdf__3 $_530 $_531)
% 0.83/1.02       true = true
% 0.83/1.02  |- ifeq (iext uri_rdf__3 $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_member $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_first $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_first $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_object $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_object $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_predicate $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_predicate $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_rest $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_rest $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_subject $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_subject $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_type $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_type $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdf_value $_530 $_531) true
% 0.83/1.02       (iext uri_rdf_value $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_comment $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_comment $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_domain $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_domain $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_isDefinedBy $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_isDefinedBy $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_isDefinedBy $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_seeAlso $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_label $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_label $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_member $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_member $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_range $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_range $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_seeAlso $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_seeAlso $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subClassOf $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_subClassOf $_530 $_531) true = true
% 0.83/1.02  |- ifeq (iext uri_rdfs_subPropertyOf $_530 $_531) true
% 0.83/1.02       (iext uri_rdfs_subPropertyOf $_530 $_531) true = true
% 0.83/1.02  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.83/1.02  
%------------------------------------------------------------------------------