Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SWB014-10 : TPTP v8.1.0. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n024.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:21 EDT 2022

% Result   : Satisfiable 0.80s 0.98s
% Output   : Saturation 0.86s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SWB014-10 : TPTP v8.1.0. Released v7.5.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n024.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Wed Jun  1 12:26:21 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.80/0.98  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/0.98  
% 0.80/0.98  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.80/0.98  |- ifeq $A $A $B $C = $B
% 0.80/0.98  |- ifeq (iext $P $S $O) true (ip $P) true = true
% 0.80/0.98  |- ir $X = true
% 0.80/0.98  |- ifeq (lv $X) true true true = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true
% 0.80/0.98  |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true
% 0.80/0.98  |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true
% 0.80/0.98  |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true
% 0.80/0.98  |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true
% 0.80/0.98  |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true
% 0.80/0.98  |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.80/0.99  |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true
% 0.80/0.99  |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true
% 0.80/0.99  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true =
% 0.80/0.99     true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true
% 0.80/0.99  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true
% 0.80/0.99       (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.80/0.99       uri_rdf_Property = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true
% 0.80/0.99  |- ifeq (icext uri_rdfs_Datatype $D) true
% 0.80/0.99       (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_domain $P $C) true
% 0.80/0.99       (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true
% 0.80/0.99  |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true
% 0.80/0.99  |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true
% 0.80/0.99  |- icext uri_rdfs_Resource $X = true
% 0.80/0.99  |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true
% 0.80/0.99  |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_range $P $C) true
% 0.80/0.99       (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.80/0.99  |- ifeq (icext $C $X) true
% 0.80/0.99       (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true =
% 0.80/0.99     true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.80/0.99  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subClassOf $D $E) true
% 0.80/0.99       (ifeq (iext uri_rdfs_subClassOf $C $D) true
% 0.80/0.99          (iext uri_rdfs_subClassOf $C $E) true) true = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.80/0.99       (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.80/0.99  |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true
% 0.80/0.99  |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true
% 0.80/0.99       (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.80/0.99          (iext uri_rdfs_subPropertyOf $P $R) true) true = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_owl_unionOf
% 0.80/0.99       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.80/0.99       sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1 =
% 0.80/0.99     true
% 0.80/0.99  |- iext uri_rdf_rest
% 0.80/0.99       sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.80/0.99       uri_rdf_nil = true
% 0.80/0.99  |- iext uri_rdf_rest
% 0.80/0.99       sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.80/0.99       sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2 =
% 0.80/0.99     true
% 0.80/0.99  |- iext uri_rdf_first
% 0.80/0.99       sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.80/0.99       uri_ex_Falcon = true
% 0.80/0.99  |- iext uri_rdf_first
% 0.80/0.99       sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.80/0.99       uri_ex_Eagle = true
% 0.80/0.99  |- iext uri_rdf_type uri_ex_Falcon uri_ex_Species = true
% 0.80/0.99  |- iext uri_rdf_type uri_ex_Eagle uri_ex_Species = true
% 0.80/0.99  |- iext uri_rdf_type uri_ex_harry
% 0.80/0.99       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u =
% 0.80/0.99     true
% 0.80/0.99  |- ~(tuple (iext uri_rdf_type $BNODE_x uri_ex_Species)
% 0.80/0.99         (iext uri_rdf_type uri_ex_harry $BNODE_x) = tuple true true)
% 0.80/0.99  |- ip uri_rdf__1 = true
% 0.80/0.99  |- ip uri_rdf__2 = true
% 0.80/0.99  |- ip uri_rdf__3 = true
% 0.80/0.99  |- ip uri_rdf_first = true
% 0.80/0.99  |- ip uri_rdf_object = true
% 0.80/0.99  |- ip uri_rdf_rest = true
% 0.80/0.99  |- ip uri_rdf_subject = true
% 0.80/0.99  |- ip uri_rdf_type = true
% 0.80/0.99  |- ip uri_rdf_value = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true
% 0.80/0.99  |- ic uri_rdfs_Container = true
% 0.80/0.99  |- ic uri_rdfs_Literal = true
% 0.80/0.99  |- ic uri_rdf_Property = true
% 0.80/0.99  |- ic uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Container = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Literal = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdf_Property = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Class = true
% 0.80/0.99  |- ic uri_rdfs_Resource = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Resource = true
% 0.80/0.99  |- ic uri_rdf_Alt = true
% 0.80/0.99  |- ic uri_rdf_Bag = true
% 0.80/0.99  |- ic uri_rdf_XMLLiteral = true
% 0.80/0.99  |- ic uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- ic uri_rdfs_Datatype = true
% 0.80/0.99  |- ic uri_rdfs_Seq = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdf_Alt = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdf_Bag = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.80/0.99       uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.80/0.99       uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Datatype = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true
% 0.80/0.99  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true
% 0.80/0.99  |- icext uri_rdfs_Class uri_rdfs_Seq = true
% 0.80/0.99  |- ip uri_rdfs_seeAlso = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true
% 0.80/0.99  |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true
% 0.80/0.99  |- ip uri_rdfs_isDefinedBy = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy =
% 0.80/0.99     true
% 0.80/0.99  |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true
% 0.80/0.99  |- icext uri_ex_Species uri_ex_Eagle = true
% 0.80/0.99  |- icext uri_ex_Species uri_ex_Falcon = true
% 0.80/0.99  |- icext
% 0.80/0.99       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.80/0.99       uri_ex_harry = true
% 0.80/0.99  |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf__1 = true
% 0.80/0.99  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf__2 = true
% 0.80/0.99  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf__3 = true
% 0.80/0.99  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_first = true
% 0.80/0.99  |- icext uri_rdf_List uri_rdf_nil = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_object = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_rest = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_subject = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_type = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdf_value = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true
% 0.80/0.99  |- icext uri_rdf_Property uri_rdfs_seeAlso = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true
% 0.80/0.99  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true
% 0.80/1.00  |- ip uri_rdfs_member = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true
% 0.80/1.00  |- icext uri_rdf_Property uri_rdfs_member = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class =
% 0.80/1.00     true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true
% 0.80/1.00  |- iext uri_rdf_type $_58 uri_rdfs_Resource = true
% 0.80/1.00  |- ~(tuple (iext uri_rdf_type uri_rdfs_Resource uri_ex_Species) true =
% 0.80/1.00       tuple true true)
% 0.80/1.00  |- ~(tuple
% 0.80/1.00         (iext uri_rdf_type
% 0.80/1.00            sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.80/1.00            uri_ex_Species) true = tuple true true)
% 0.80/1.00  |- ~(tuple true (iext uri_rdf_type uri_ex_harry uri_ex_Eagle) =
% 0.80/1.00       tuple true true)
% 0.80/1.00  |- ~(tuple true (iext uri_rdf_type uri_ex_harry uri_ex_Falcon) =
% 0.80/1.00       tuple true true)
% 0.80/1.00  |- ifeq (iext uri_rdf__1 $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf__2 $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf__3 $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_first $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_object $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_rest $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_subject $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_type $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdf_value $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_isDefinedBy $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_member $_80 $_78) true true true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_seeAlso $_80 $_78) true true true = true
% 0.80/1.00  |- ip uri_owl_unionOf = true
% 0.80/1.00  |- ip uri_rdfs_domain = true
% 0.80/1.00  |- ip uri_rdfs_range = true
% 0.80/1.00  |- ip uri_rdfs_subClassOf = true
% 0.80/1.00  |- ip uri_rdfs_subPropertyOf = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_domain $S $O) true true true = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_range $S $O) true true true = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf =
% 0.80/1.00     true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.80/1.00       uri_rdfs_subPropertyOf = true
% 0.80/1.00  |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.80/1.00  |- icext uri_rdf_Property uri_rdfs_domain = true
% 0.80/1.00  |- ifeq (iext uri_owl_unionOf $S $O) true true true = true
% 0.80/1.00  |- iext uri_rdfs_subPropertyOf uri_owl_unionOf uri_owl_unionOf = true
% 0.80/1.00  |- iext uri_rdf_type uri_owl_unionOf uri_rdf_Property = true
% 0.80/1.00  |- icext uri_rdf_Property uri_owl_unionOf = true
% 0.80/1.00  |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true
% 0.80/1.00  |- icext uri_rdf_Property uri_rdfs_range = true
% 0.80/1.00  |- icext uri_rdf_Property uri_rdfs_subClassOf = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_Alt $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_Alt $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_Bag $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_Bag $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_Property $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Class $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Container $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_117)
% 0.80/1.00       true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_117)
% 0.80/1.00       true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Literal $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_117) true
% 0.80/1.00       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_117) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_Alt) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Container) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_Alt) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_Bag) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Container) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_Bag) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_Property) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_XMLLiteral) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Literal) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdf_XMLLiteral) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Class) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Container) true
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.00  |- ifeq
% 0.80/1.00       (iext uri_rdfs_subClassOf $_115 uri_rdfs_ContainerMembershipProperty)
% 0.80/1.00       true (iext uri_rdfs_subClassOf $_115 uri_rdf_Property) true = true
% 0.80/1.01  |- ifeq
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_ContainerMembershipProperty)
% 0.80/1.01       true (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Datatype) true
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Class) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Datatype) true
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Literal) true
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Seq) true
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Container) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subClassOf $_115 uri_rdfs_Seq) true
% 0.80/1.01       (iext uri_rdfs_subClassOf $_115 uri_rdfs_Resource) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_174) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf uri_rdf__1 $_174) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_174) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf uri_rdf__2 $_174) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_174) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf uri_rdf__3 $_174) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_174) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_174) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_172 uri_rdf__1) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf $_172 uri_rdfs_member) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_172 uri_rdf__2) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf $_172 uri_rdfs_member) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_172 uri_rdf__3) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf $_172 uri_rdfs_member) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_subPropertyOf $_172 uri_rdfs_isDefinedBy) true
% 0.80/1.01       (iext uri_rdfs_subPropertyOf $_172 uri_rdfs_seeAlso) true = true
% 0.80/1.01  |- ifeq
% 0.80/1.01       (iext uri_rdfs_domain $_218
% 0.80/1.01          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.80/1.01       true (ifeq (iext $_218 uri_ex_harry $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_ex_Species) true
% 0.80/1.01       (ifeq (iext $_218 uri_ex_Eagle $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_ex_Species) true
% 0.80/1.01       (ifeq (iext $_218 uri_ex_Falcon $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_List) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_nil $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_owl_unionOf $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf__1 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf__2 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf__3 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_first $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_object $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_rest $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_subject $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_type $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_value $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_domain $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_isDefinedBy $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_member $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_range $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_seeAlso $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_subClassOf $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdf_Property) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_subPropertyOf $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_Alt $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_Bag $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_Property $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_XMLLiteral $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Class $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Container $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_ContainerMembershipProperty $_220) true
% 0.80/1.01          true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Datatype $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Literal $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Resource $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Class) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdfs_Seq $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_ContainerMembershipProperty)
% 0.80/1.01       true (ifeq (iext $_218 uri_rdf__1 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_ContainerMembershipProperty)
% 0.80/1.01       true (ifeq (iext $_218 uri_rdf__2 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_ContainerMembershipProperty)
% 0.80/1.01       true (ifeq (iext $_218 uri_rdf__3 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Datatype) true
% 0.80/1.01       (ifeq (iext $_218 uri_rdf_XMLLiteral $_220) true true true) true =
% 0.80/1.01     true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain $_218 uri_rdfs_Resource) true
% 0.80/1.01       (ifeq (iext $_218 $_219 $_220) true true true) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_owl_unionOf $_217) true
% 0.80/1.01       (icext $_217
% 0.80/1.01          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_217) true
% 0.80/1.01       (icext $_217
% 0.80/1.01          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_217) true
% 0.80/1.01       (icext $_217
% 0.80/1.01          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_217) true
% 0.80/1.01       (icext $_217
% 0.80/1.01          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_217) true
% 0.80/1.01       (icext $_217
% 0.80/1.01          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdf_type $_217) true (icext $_217 $_219)
% 0.80/1.01       true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__1) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__2) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__3) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_first) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_object) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_predicate) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_rest) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_subject) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_type) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_value) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_comment) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_domain) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_isDefinedBy) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_label) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_member) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_range) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_seeAlso) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_subClassOf) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_subPropertyOf) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__1) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__2) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__3) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_first) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_predicate) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_rest) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_subject) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_type) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_value) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_comment) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_domain) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_isDefinedBy) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_label) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_member) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_range) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_seeAlso) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_subClassOf) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_subPropertyOf) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_Alt) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_Bag) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_Property) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf_XMLLiteral) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Class) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Container) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_ContainerMembershipProperty) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Datatype) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Literal) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Resource) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdfs_Seq) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.01       (icext $_217 uri_owl_unionOf) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__1) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__2) true = true
% 0.80/1.01  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.01       (icext $_217 uri_rdf__3) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_first) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_object) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_rest) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_subject) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_type) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdf_value) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_domain) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_isDefinedBy) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_member) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_range) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_seeAlso) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_subClassOf) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_217) true
% 0.80/1.02       (icext $_217 uri_rdfs_subPropertyOf) true = true
% 0.80/1.02  |- ifeq (iext uri_rdf_first $_219 $_220) true (icext uri_rdf_List $_219)
% 0.80/1.02       true = true
% 0.80/1.02  |- ifeq (iext uri_rdf_object $_219 $_220) true
% 0.80/1.02       (icext uri_rdfs_Statement $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdf_predicate $_219 $_220) true
% 0.80/1.02       (icext uri_rdfs_Statement $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdf_rest $_219 $_220) true (icext uri_rdf_List $_219)
% 0.80/1.02       true = true
% 0.80/1.02  |- ifeq (iext uri_rdf_subject $_219 $_220) true
% 0.80/1.02       (icext uri_rdfs_Statement $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_comment $_219 $_220) true true true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $_219 $_220) true
% 0.80/1.02       (icext uri_rdf_Property $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_label $_219 $_220) true true true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_219 $_220) true
% 0.80/1.02       (icext uri_rdf_Property $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_subClassOf $_219 $_220) true
% 0.80/1.02       (icext uri_rdfs_Class $_219) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_subPropertyOf $_219 $_220) true
% 0.80/1.02       (icext uri_rdf_Property $_219) true = true
% 0.80/1.02  |- icext uri_rdf_List
% 0.80/1.02       sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2 =
% 0.80/1.02     true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.80/1.02       (ifeq
% 0.80/1.02          (iext $P
% 0.80/1.02             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.80/1.02             $Y) true true true) true = true
% 0.80/1.02  |- iext uri_rdf_type
% 0.80/1.02       sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.80/1.02       uri_rdf_List = true
% 0.80/1.02  |- icext uri_rdf_List
% 0.80/1.02       sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1 =
% 0.80/1.02     true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.80/1.02       (ifeq
% 0.80/1.02          (iext $P
% 0.80/1.02             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.80/1.02             $Y) true true true) true = true
% 0.80/1.02  |- iext uri_rdf_type
% 0.80/1.02       sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.80/1.02       uri_rdf_List = true
% 0.80/1.02  |- icext uri_rdf_Property uri_rdf_predicate = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true
% 0.80/1.02  |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true
% 0.80/1.02  |- ip uri_rdf_predicate = true
% 0.80/1.02  |- ifeq (iext uri_rdf_predicate $S $O) true true true = true
% 0.80/1.02  |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.80/1.02       (icext $C uri_rdf_predicate) true = true
% 0.80/1.02  |- icext uri_rdf_Property uri_rdfs_comment = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true
% 0.80/1.02  |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true
% 0.80/1.02  |- ip uri_rdfs_comment = true
% 0.80/1.02  |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.80/1.02       (icext $C uri_rdfs_comment) true = true
% 0.80/1.02  |- icext uri_rdf_Property uri_rdfs_label = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true
% 0.80/1.02  |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true
% 0.80/1.02  |- ip uri_rdfs_label = true
% 0.80/1.02  |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.80/1.02       (icext $C uri_rdfs_label) true = true
% 0.80/1.02  |- ifeq
% 0.80/1.02       (iext uri_rdfs_range $_327
% 0.80/1.02          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.80/1.02       true (ifeq (iext $_327 $_328 uri_ex_harry) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_ex_Species) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_ex_Eagle) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_ex_Species) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_ex_Falcon) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_List) true
% 0.80/1.02       (ifeq
% 0.80/1.02          (iext $_327 $_328
% 0.80/1.02             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.80/1.02          true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_List) true
% 0.80/1.02       (ifeq
% 0.80/1.02          (iext $_327 $_328
% 0.80/1.02             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.80/1.02          true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_List) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_nil) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_owl_unionOf) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf__1) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf__2) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf__3) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_first) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_object) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_predicate) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_rest) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_subject) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_type) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_value) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_comment) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_domain) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_isDefinedBy) true true true) true =
% 0.80/1.02     true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_label) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_member) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_range) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_seeAlso) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_subClassOf) true true true) true =
% 0.80/1.02     true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdf_Property) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdfs_subPropertyOf) true true true) true =
% 0.80/1.02     true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_Alt) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_Bag) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_Property) true true true) true = true
% 0.80/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.80/1.02       (ifeq (iext $_327 $_328 uri_rdf_XMLLiteral) true true true) true =
% 0.80/1.02     true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Class) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Container) true true true) true =
% 0.86/1.02     true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_ContainerMembershipProperty) true
% 0.86/1.02          true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Datatype) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Literal) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Resource) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Class) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdfs_Seq) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.02       true (ifeq (iext $_327 $_328 uri_rdf__1) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.02       true (ifeq (iext $_327 $_328 uri_rdf__2) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.02       true (ifeq (iext $_327 $_328 uri_rdf__3) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Datatype) true
% 0.86/1.02       (ifeq (iext $_327 $_328 uri_rdf_XMLLiteral) true true true) true =
% 0.86/1.02     true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_327 uri_rdfs_Resource) true
% 0.86/1.02       (ifeq (iext $_327 $_328 $_329) true true true) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_owl_unionOf $_326) true
% 0.86/1.02       (icext $_326
% 0.86/1.02          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_first $_326) true
% 0.86/1.02       (icext $_326 uri_ex_Falcon) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_first $_326) true
% 0.86/1.02       (icext $_326 uri_ex_Eagle) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_nil) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_326) true
% 0.86/1.02       (icext $_326
% 0.86/1.02          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_List) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_ex_Species) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326
% 0.86/1.02          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Property) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Class) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Datatype) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_ContainerMembershipProperty) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdf_type $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Resource) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Resource) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_List) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Statement) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Property) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Class) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Resource) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_List) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Class) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Literal) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Property) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Alt) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Container) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Resource) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Bag) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_Property) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_XMLLiteral) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Literal) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Class) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_ContainerMembershipProperty) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Datatype) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_Seq) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_owl_unionOf) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf__1) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_member) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf__2) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf__3) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_first) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_object) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_predicate) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_rest) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_subject) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_type) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdf_value) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_comment) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_domain) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_isDefinedBy) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_seeAlso) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_label) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_range) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_subClassOf) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_326) true
% 0.86/1.02       (icext $_326 uri_rdfs_subPropertyOf) true = true
% 0.86/1.02  |- ifeq (iext uri_rdf_rest $_328 $_329) true (icext uri_rdf_List $_329)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdf_type $_328 $_329) true (icext uri_rdfs_Class $_329)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_comment $_328 $_329) true
% 0.86/1.02       (icext uri_rdfs_Literal $_329) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_domain $_328 $_329) true
% 0.86/1.02       (icext uri_rdfs_Class $_329) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_label $_328 $_329) true
% 0.86/1.02       (icext uri_rdfs_Literal $_329) true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_range $_328 $_329) true (icext uri_rdfs_Class $_329)
% 0.86/1.02       true = true
% 0.86/1.02  |- ifeq (iext uri_rdfs_subClassOf $_328 $_329) true
% 0.86/1.02       (icext uri_rdfs_Class $_329) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_328 $_329) true
% 0.86/1.03       (icext uri_rdf_Property $_329) true = true
% 0.86/1.03  |- icext uri_rdfs_Class uri_rdf_List = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P $X uri_rdf_List) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P uri_rdf_List $Y) true true true) true = true
% 0.86/1.03  |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true
% 0.86/1.03  |- ic uri_rdf_List = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_rdf_List) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_rdf_List) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true
% 0.86/1.03       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.86/1.03       (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true
% 0.86/1.03  |- icext uri_rdfs_Class uri_ex_Species = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P $X uri_ex_Species) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P uri_ex_Species $Y) true true true) true = true
% 0.86/1.03  |- iext uri_rdf_type uri_ex_Species uri_rdfs_Class = true
% 0.86/1.03  |- ic uri_ex_Species = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_ex_Species uri_ex_Species = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_ex_Species uri_rdfs_Resource = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_ex_Species) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_ex_Species) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf $C uri_ex_Species) true
% 0.86/1.03       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.86/1.03       (iext uri_rdfs_subClassOf uri_ex_Species $E) true = true
% 0.86/1.03  |- icext uri_rdfs_Class
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $P $X
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $P
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03             $Y) true true true) true = true
% 0.86/1.03  |- iext uri_rdf_type
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03       uri_rdfs_Class = true
% 0.86/1.03  |- ic
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u =
% 0.86/1.03     true
% 0.86/1.03  |- iext uri_rdfs_subClassOf
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u =
% 0.86/1.03     true
% 0.86/1.03  |- iext uri_rdfs_subClassOf
% 0.86/1.03       sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03       uri_rdfs_Resource = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C
% 0.86/1.03          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C
% 0.86/1.03          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq
% 0.86/1.03       (iext uri_rdfs_subClassOf $C
% 0.86/1.03          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03       true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.86/1.03       (iext uri_rdfs_subClassOf
% 0.86/1.03          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03          $E) true = true
% 0.86/1.03  |- icext uri_rdfs_Class uri_rdfs_Statement = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.86/1.03       (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true
% 0.86/1.03  |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true
% 0.86/1.03  |- ic uri_rdfs_Statement = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true
% 0.86/1.03  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_rdfs_Statement) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.86/1.03       (icext $C uri_rdfs_Statement) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true
% 0.86/1.03       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.86/1.03       (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_owl_unionOf) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_first) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.03             uri_ex_Falcon) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_first) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.03             uri_ex_Eagle) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_rest) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.03             uri_rdf_nil) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_rest) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.03             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.03             uri_rdf_List) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03             uri_rdfs_Class) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.03             uri_rdf_List) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_ex_Eagle uri_ex_Species) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_ex_Falcon uri_ex_Species) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_ex_Species uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424 uri_ex_harry
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_owl_unionOf uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Alt uri_rdfs_Class) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Bag uri_rdfs_Class) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_List uri_rdfs_Class) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Property uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_XMLLiteral uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__1 uri_rdf_Property) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__1 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__2 uri_rdf_Property) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__2 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__3 uri_rdf_Property) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__3 uri_rdfs_ContainerMembershipProperty)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_first uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_nil uri_rdf_List) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_object uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_predicate uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_rest uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_subject uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_type uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_value uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Container uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Literal uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Resource uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Seq uri_rdfs_Class) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Statement uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_comment uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_isDefinedBy uri_rdf_Property) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_label uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_member uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_range uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_seeAlso uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subClassOf uri_rdf_Property) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdf_type) true
% 0.86/1.03       (ifeq (iext $_424 $_426 uri_rdfs_Resource) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_first uri_rdf_List) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_object uri_rdfs_Statement) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_predicate uri_rdfs_Statement) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_subject uri_rdfs_Statement) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_type uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_comment uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_label uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_range uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_domain) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_first uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_predicate uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_subject uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_type uri_rdfs_Class) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_comment uri_rdfs_Literal) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_domain uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_label uri_rdfs_Literal) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_range uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_range) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.03          true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq
% 0.86/1.03          (iext $_424
% 0.86/1.03             sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.03             uri_rdfs_Resource) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_ex_Species uri_ex_Species) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_ex_Species uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Alt uri_rdf_Alt) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Alt uri_rdfs_Container) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Alt uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Bag uri_rdf_Bag) true true true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Bag uri_rdfs_Container) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Bag uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_List uri_rdf_List) true true true) true =
% 0.86/1.03     true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_List uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Property uri_rdf_Property) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_Property uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdf_XMLLiteral uri_rdfs_Resource) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Class uri_rdfs_Resource) true true true)
% 0.86/1.03       true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Container uri_rdfs_Container) true true
% 0.86/1.03          true) true = true
% 0.86/1.03  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.03       (ifeq (iext $_424 uri_rdfs_Container uri_rdfs_Resource) true true
% 0.86/1.03          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq
% 0.86/1.04          (iext $_424 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.86/1.04          true true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq
% 0.86/1.04          (iext $_424 uri_rdfs_ContainerMembershipProperty
% 0.86/1.04             uri_rdfs_ContainerMembershipProperty) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq
% 0.86/1.04          (iext $_424 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.86/1.04          true true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Datatype uri_rdfs_Datatype) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Datatype uri_rdfs_Resource) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Literal uri_rdfs_Literal) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Literal uri_rdfs_Resource) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Resource uri_rdfs_Resource) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Seq uri_rdfs_Container) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Seq uri_rdfs_Resource) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Seq uri_rdfs_Seq) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Statement uri_rdfs_Resource) true true
% 0.86/1.04          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subClassOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_Statement uri_rdfs_Statement) true true
% 0.86/1.04          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_owl_unionOf uri_owl_unionOf) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__1 uri_rdf__1) true true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__1 uri_rdfs_member) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__2 uri_rdf__2) true true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__2 uri_rdfs_member) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__3 uri_rdf__3) true true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf__3 uri_rdfs_member) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_first uri_rdf_first) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_object uri_rdf_object) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_predicate uri_rdf_predicate) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_rest uri_rdf_rest) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_subject uri_rdf_subject) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_type uri_rdf_type) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdf_value uri_rdf_value) true true true) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_comment uri_rdfs_comment) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_domain uri_rdfs_domain) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true
% 0.86/1.04          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true
% 0.86/1.04          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_label uri_rdfs_label) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_member uri_rdfs_member) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_range uri_rdfs_range) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true
% 0.86/1.04          true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $_424 uri_rdfs_subPropertyOf) true
% 0.86/1.04       (ifeq (iext $_424 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true
% 0.86/1.04          true true) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_unionOf $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.04          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.04          uri_ex_Falcon) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.04          uri_ex_Eagle) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.04          uri_rdf_nil) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.04          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2
% 0.86/1.04          uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.04          uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1
% 0.86/1.04          uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_ex_Eagle uri_ex_Species) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_ex_Falcon uri_ex_Species) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_ex_Species uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_ex_harry
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_owl_unionOf uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Alt uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Bag uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_List uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Property uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_XMLLiteral uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__1 uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__2 uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__3 uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true =
% 0.86/1.04     true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_first uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_nil uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_object uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_predicate uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_rest uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_subject uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_type uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_value uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Container uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Literal uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Resource uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Seq uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_Statement uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_comment uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_domain uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_isDefinedBy uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_label uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_member uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_range uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_seeAlso uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subClassOf uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_425) true
% 0.86/1.04       (iext $_425 $_426 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_first uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_object uri_rdfs_Statement) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_predicate uri_rdfs_Statement) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_rest uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_subject uri_rdfs_Statement) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_type uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_value uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_comment uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_domain uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_label uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_range uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_first uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_predicate uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_rest uri_rdf_List) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_subject uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_type uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_value uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_comment uri_rdfs_Literal) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_domain uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_label uri_rdfs_Literal) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_range uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_425) true
% 0.86/1.04       (iext $_425 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.04       true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425
% 0.86/1.04          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.04          uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_ex_Species uri_ex_Species) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_ex_Species uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Alt uri_rdf_Alt) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Alt uri_rdfs_Container) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Alt uri_rdfs_Resource) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Bag uri_rdf_Bag) true = true
% 0.86/1.04  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.04       (iext $_425 uri_rdf_Bag uri_rdfs_Container) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_Bag uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_List uri_rdf_List) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_List uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_Property uri_rdf_Property) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_Property uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Class uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Container uri_rdfs_Container) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Container uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_ContainerMembershipProperty
% 0.86/1.05          uri_rdfs_ContainerMembershipProperty) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Datatype uri_rdfs_Datatype) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Datatype uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Literal uri_rdfs_Literal) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Literal uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Resource uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Seq uri_rdfs_Container) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Seq uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Seq uri_rdfs_Seq) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Statement uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_Statement uri_rdfs_Statement) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_owl_unionOf uri_owl_unionOf) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__1 uri_rdf__1) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__1 uri_rdfs_member) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__2 uri_rdf__2) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__2 uri_rdfs_member) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__3 uri_rdf__3) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf__3 uri_rdfs_member) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_first uri_rdf_first) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_object uri_rdf_object) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_predicate uri_rdf_predicate) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_rest uri_rdf_rest) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_subject uri_rdf_subject) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_type uri_rdf_type) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdf_value uri_rdf_value) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_comment uri_rdfs_comment) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_domain uri_rdfs_domain) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_label uri_rdfs_label) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_member uri_rdfs_member) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_range uri_rdfs_range) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_425) true
% 0.86/1.05       (iext $_425 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true
% 0.86/1.05  |- ifeq (iext uri_owl_unionOf $_426 $_427) true
% 0.86/1.05       (iext uri_owl_unionOf $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__1 $_426 $_427) true (iext uri_rdf__1 $_426 $_427)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__1 $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_member $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__2 $_426 $_427) true (iext uri_rdf__2 $_426 $_427)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__2 $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_member $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__3 $_426 $_427) true (iext uri_rdf__3 $_426 $_427)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdf__3 $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_member $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_first $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_first $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_object $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_object $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_predicate $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_predicate $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_rest $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_rest $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_subject $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_subject $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_type $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_type $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdf_value $_426 $_427) true
% 0.86/1.05       (iext uri_rdf_value $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_comment $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_comment $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_domain $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_domain $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_isDefinedBy $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_isDefinedBy $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_isDefinedBy $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_seeAlso $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_label $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_label $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_member $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_member $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_range $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_range $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_seeAlso $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_seeAlso $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_subClassOf $_426 $_427) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subPropertyOf $_426 $_427) true
% 0.86/1.05       (iext uri_rdfs_subPropertyOf $_426 $_427) true = true
% 0.86/1.05  |- ifeq (icext $_945 $_947) true true true = true
% 0.86/1.05  |- ifeq
% 0.86/1.05       (icext
% 0.86/1.05          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.05          $_947) true
% 0.86/1.05       (icext
% 0.86/1.05          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.05          $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_ex_Species $_947) true (icext uri_ex_Species $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdf_Alt $_947) true (icext uri_rdf_Alt $_947) true =
% 0.86/1.05     true
% 0.86/1.05  |- ifeq (icext uri_rdf_Alt $_947) true (icext uri_rdfs_Container $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdf_Bag $_947) true (icext uri_rdf_Bag $_947) true =
% 0.86/1.05     true
% 0.86/1.05  |- ifeq (icext uri_rdf_Bag $_947) true (icext uri_rdfs_Container $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdf_List $_947) true (icext uri_rdf_List $_947) true =
% 0.86/1.05     true
% 0.86/1.05  |- ifeq (icext uri_rdf_Property $_947) true (icext uri_rdf_Property $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdf_XMLLiteral $_947) true
% 0.86/1.05       (icext uri_rdf_XMLLiteral $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdf_XMLLiteral $_947) true
% 0.86/1.05       (icext uri_rdfs_Literal $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Class $_947) true (icext uri_rdfs_Class $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Container $_947) true
% 0.86/1.05       (icext uri_rdfs_Container $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_947) true
% 0.86/1.05       (icext uri_rdf_Property $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_947) true
% 0.86/1.05       (icext uri_rdfs_ContainerMembershipProperty $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Datatype $_947) true (icext uri_rdfs_Class $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Datatype $_947) true
% 0.86/1.05       (icext uri_rdfs_Datatype $_947) true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Literal $_947) true (icext uri_rdfs_Literal $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Seq $_947) true (icext uri_rdfs_Container $_947)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Seq $_947) true (icext uri_rdfs_Seq $_947) true =
% 0.86/1.05     true
% 0.86/1.05  |- ifeq (icext uri_rdfs_Statement $_947) true
% 0.86/1.05       (icext uri_rdfs_Statement $_947) true = true
% 0.86/1.05  |- ifeq
% 0.86/1.05       (iext uri_rdfs_subClassOf
% 0.86/1.05          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u
% 0.86/1.05          $_946) true (icext $_946 uri_ex_harry) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_ex_Species $_946) true
% 0.86/1.05       (icext $_946 uri_ex_Eagle) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_ex_Species $_946) true
% 0.86/1.05       (icext $_946 uri_ex_Falcon) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_946) true
% 0.86/1.05       (icext $_946
% 0.86/1.05          sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_946) true
% 0.86/1.05       (icext $_946
% 0.86/1.05          sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_nil) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_owl_unionOf) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf__1) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf__2) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf__3) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_first) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_object) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_predicate) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_rest) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_subject) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_type) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_value) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_comment) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_domain) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_isDefinedBy) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_label) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_member) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_range) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_seeAlso) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_subClassOf) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_subPropertyOf) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946
% 0.86/1.05          sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)
% 0.86/1.05       true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_ex_Species) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_Alt) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_Bag) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_List) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_Property) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_XMLLiteral) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Class) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Container) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_ContainerMembershipProperty) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Datatype) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Literal) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Resource) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Seq) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_946) true
% 0.86/1.05       (icext $_946 uri_rdfs_Statement) true = true
% 0.86/1.05  |- ifeq
% 0.86/1.05       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_946)
% 0.86/1.05       true (icext $_946 uri_rdf__1) true = true
% 0.86/1.05  |- ifeq
% 0.86/1.05       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_946)
% 0.86/1.05       true (icext $_946 uri_rdf__2) true = true
% 0.86/1.05  |- ifeq
% 0.86/1.05       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_946)
% 0.86/1.05       true (icext $_946 uri_rdf__3) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_946) true
% 0.86/1.05       (icext $_946 uri_rdf_XMLLiteral) true = true
% 0.86/1.05  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_946) true
% 0.86/1.05       (icext $_946 $_947) true = true
% 0.86/1.05  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.86/1.05  
%------------------------------------------------------------------------------