↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SWB020-10 : TPTP v8.1.0. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n019.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:24 EDT 2022

% Result   : Satisfiable 0.83s 1.04s
% Output   : Saturation 0.90s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11  % Problem  : SWB020-10 : TPTP v8.1.0. Released v7.3.0.
% 0.10/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n019.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 600
% 0.12/0.33  % DateTime : Wed Jun  1 09:30:40 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.33  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.83/1.04  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.83/1.04  
% 0.83/1.04  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.83/1.04  |- ifeq $A $A $B $C = $B
% 0.83/1.04  |- ifeq (iext $P $S $O) true (ip $P) true = true
% 0.83/1.04  |- ir $X = true
% 0.83/1.04  |- ifeq (lv $X) true true true = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true
% 0.83/1.04  |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true
% 0.83/1.04  |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.83/1.04  |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true
% 0.83/1.04  |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true
% 0.83/1.04  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true
% 0.83/1.04  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true
% 0.83/1.04       (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.83/1.04       uri_rdf_Property = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true
% 0.83/1.04  |- ifeq (icext uri_rdfs_Datatype $D) true
% 0.83/1.04       (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_domain $P $C) true
% 0.83/1.04       (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true
% 0.83/1.04  |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true
% 0.83/1.04  |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true
% 0.83/1.04  |- icext uri_rdfs_Resource $X = true
% 0.83/1.04  |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true
% 0.83/1.04  |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true
% 0.83/1.04  |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_range $P $C) true
% 0.83/1.04       (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.83/1.04  |- ifeq (icext $C $X) true
% 0.83/1.04       (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true =
% 0.83/1.04     true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.83/1.04  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subClassOf $D $E) true
% 0.83/1.04       (ifeq (iext uri_rdfs_subClassOf $C $D) true
% 0.83/1.04          (iext uri_rdfs_subClassOf $C $E) true) true = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.83/1.04       (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.83/1.04  |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true
% 0.83/1.04  |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true
% 0.83/1.04       (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.83/1.04          (iext uri_rdfs_subPropertyOf $P $R) true) true = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true
% 0.83/1.04  |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true
% 0.83/1.04  |- iext uri_owl_complementOf
% 0.83/1.04       sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc
% 0.83/1.04       uri_ex_c2 = true
% 0.83/1.04  |- iext uri_owl_intersectionOf
% 0.83/1.04       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.04       sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1 =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_owl_disjointWith uri_ex_d uri_ex_c1 = true
% 0.83/1.04  |- iext uri_owl_unionOf uri_ex_c
% 0.83/1.04       sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1 =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_rdf_rest
% 0.83/1.04       sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.83/1.04       uri_rdf_nil = true
% 0.83/1.04  |- iext uri_rdf_rest
% 0.83/1.04       sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.83/1.04       sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2 =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_rdf_rest
% 0.83/1.04       sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.83/1.04       sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3 =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_rdf_rest
% 0.83/1.04       sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.83/1.04       uri_rdf_nil = true
% 0.83/1.04  |- iext uri_rdf_rest
% 0.83/1.04       sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.83/1.04       sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2 =
% 0.83/1.04     true
% 0.83/1.04  |- iext uri_rdf_first
% 0.83/1.04       sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.83/1.04       uri_ex_c3 = true
% 0.83/1.04  |- iext uri_rdf_first
% 0.83/1.04       sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.83/1.04       uri_ex_c1 = true
% 0.83/1.04  |- iext uri_rdf_first
% 0.83/1.04       sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.83/1.04       uri_ex_c2 = true
% 0.83/1.04  |- iext uri_rdf_first
% 0.83/1.04       sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.83/1.04       sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc = true
% 0.83/1.04  |- iext uri_rdf_first
% 0.83/1.04       sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.83/1.04       uri_ex_c = true
% 0.83/1.04  |- iext uri_rdfs_subClassOf uri_ex_d
% 0.83/1.04       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs = true
% 0.83/1.04  |- ~(iext uri_rdfs_subClassOf uri_ex_d uri_ex_c3 = true)
% 0.83/1.04  |- ip uri_rdf__1 = true
% 0.83/1.04  |- ip uri_rdf__2 = true
% 0.83/1.04  |- ip uri_rdf__3 = true
% 0.83/1.05  |- ip uri_rdf_first = true
% 0.83/1.05  |- ip uri_rdf_object = true
% 0.83/1.05  |- ip uri_rdf_rest = true
% 0.83/1.05  |- ip uri_rdf_subject = true
% 0.83/1.05  |- ip uri_rdf_type = true
% 0.83/1.05  |- ip uri_rdf_value = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true
% 0.83/1.05  |- ic uri_ex_d = true
% 0.83/1.05  |- ic uri_rdf_Alt = true
% 0.83/1.05  |- ic uri_rdf_Bag = true
% 0.83/1.05  |- ic uri_rdf_XMLLiteral = true
% 0.83/1.05  |- ic uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.05  |- ic uri_rdfs_Datatype = true
% 0.83/1.05  |- ic uri_rdfs_Seq = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_ex_d uri_ex_d = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_ex_d uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_ex_d = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdf_Alt = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdf_Bag = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.83/1.05       uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.83/1.05       uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Datatype = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Seq = true
% 0.83/1.05  |- ip uri_rdfs_seeAlso = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true
% 0.83/1.05  |- ic sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs =
% 0.83/1.05     true
% 0.83/1.05  |- ic uri_rdfs_Resource = true
% 0.83/1.05  |- ic uri_rdfs_Container = true
% 0.83/1.05  |- ic uri_rdfs_Literal = true
% 0.83/1.05  |- ic uri_rdf_Property = true
% 0.83/1.05  |- ic uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf
% 0.83/1.05       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.05       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf
% 0.83/1.05       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.05       uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class
% 0.83/1.05       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Resource = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Container = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Literal = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdf_Property = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Class uri_rdfs_Class = true
% 0.83/1.05  |- ip uri_rdfs_isDefinedBy = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy =
% 0.83/1.05     true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true
% 0.83/1.05  |- iext uri_rdf_type
% 0.83/1.05       sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.05       uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_ex_d uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class =
% 0.83/1.05     true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true
% 0.83/1.05  |- iext uri_rdf_type $_60 uri_rdfs_Resource = true
% 0.83/1.05  |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf__1 = true
% 0.83/1.05  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf__2 = true
% 0.83/1.05  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf__3 = true
% 0.83/1.05  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_first = true
% 0.83/1.05  |- icext uri_rdf_List uri_rdf_nil = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_object = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_rest = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_subject = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_type = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdf_value = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdfs_seeAlso = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true
% 0.83/1.05  |- ip uri_rdfs_member = true
% 0.83/1.05  |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true
% 0.83/1.05  |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true
% 0.83/1.05  |- icext uri_rdf_Property uri_rdfs_member = true
% 0.83/1.05  |- ifeq (iext uri_rdf__1 $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf__2 $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf__3 $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_first $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_object $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_rest $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_subject $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_type $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdf_value $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdfs_isDefinedBy $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdfs_member $_82 $_80) true true true = true
% 0.83/1.05  |- ifeq (iext uri_rdfs_seeAlso $_82 $_80) true true true = true
% 0.83/1.05  |- ip uri_owl_complementOf = true
% 0.83/1.05  |- ip uri_owl_disjointWith = true
% 0.83/1.05  |- ip uri_owl_intersectionOf = true
% 0.83/1.05  |- ip uri_owl_unionOf = true
% 0.83/1.05  |- ip uri_rdfs_domain = true
% 0.83/1.05  |- ip uri_rdfs_range = true
% 0.83/1.05  |- ip uri_rdfs_subClassOf = true
% 0.83/1.05  |- ip uri_rdfs_subPropertyOf = true
% 0.83/1.05  |- ifeq (iext uri_owl_disjointWith $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_owl_disjointWith uri_owl_disjointWith =
% 0.83/1.06     true
% 0.83/1.06  |- iext uri_rdf_type uri_owl_disjointWith uri_rdf_Property = true
% 0.83/1.06  |- ifeq (iext uri_owl_intersectionOf $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_owl_intersectionOf
% 0.83/1.06       uri_owl_intersectionOf = true
% 0.83/1.06  |- iext uri_rdf_type uri_owl_intersectionOf uri_rdf_Property = true
% 0.83/1.06  |- ifeq (iext uri_owl_unionOf $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_owl_unionOf uri_owl_unionOf = true
% 0.83/1.06  |- iext uri_rdf_type uri_owl_unionOf uri_rdf_Property = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true
% 0.83/1.06  |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf =
% 0.83/1.06     true
% 0.83/1.06  |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.83/1.06       uri_rdfs_subPropertyOf = true
% 0.83/1.06  |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.83/1.06  |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true
% 0.83/1.06  |- icext uri_rdf_Property uri_owl_disjointWith = true
% 0.83/1.06  |- icext uri_rdf_Property uri_owl_intersectionOf = true
% 0.83/1.06  |- icext uri_rdf_Property uri_owl_unionOf = true
% 0.83/1.06  |- icext uri_rdf_Property uri_rdfs_domain = true
% 0.83/1.06  |- ifeq (iext uri_owl_complementOf $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_owl_complementOf uri_owl_complementOf =
% 0.83/1.06     true
% 0.83/1.06  |- iext uri_rdf_type uri_owl_complementOf uri_rdf_Property = true
% 0.83/1.06  |- icext uri_rdf_Property uri_owl_complementOf = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_range $S $O) true true true = true
% 0.83/1.06  |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true
% 0.83/1.06  |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true
% 0.83/1.06  |- icext uri_rdf_Property uri_rdfs_range = true
% 0.83/1.06  |- icext uri_rdf_Property uri_rdfs_subClassOf = true
% 0.83/1.06  |- ifeq (icext $_123 $_125) true true true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (icext sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06          $_125) true
% 0.83/1.06       (icext sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06          $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_ex_d $_125) true
% 0.83/1.06       (icext sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06          $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_ex_d $_125) true (icext uri_ex_d $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdf_Alt $_125) true (icext uri_rdf_Alt $_125) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (icext uri_rdf_Alt $_125) true (icext uri_rdfs_Container $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdf_Bag $_125) true (icext uri_rdf_Bag $_125) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (icext uri_rdf_Bag $_125) true (icext uri_rdfs_Container $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdf_Property $_125) true (icext uri_rdf_Property $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdf_XMLLiteral $_125) true
% 0.83/1.06       (icext uri_rdf_XMLLiteral $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdf_XMLLiteral $_125) true
% 0.83/1.06       (icext uri_rdfs_Literal $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Class $_125) true (icext uri_rdfs_Class $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Container $_125) true
% 0.83/1.06       (icext uri_rdfs_Container $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_125) true
% 0.83/1.06       (icext uri_rdf_Property $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_125) true
% 0.83/1.06       (icext uri_rdfs_ContainerMembershipProperty $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Datatype $_125) true (icext uri_rdfs_Class $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Datatype $_125) true
% 0.83/1.06       (icext uri_rdfs_Datatype $_125) true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Literal $_125) true (icext uri_rdfs_Literal $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Seq $_125) true (icext uri_rdfs_Container $_125)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (icext uri_rdfs_Seq $_125) true (icext uri_rdfs_Seq $_125) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_nil) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_owl_complementOf) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_owl_disjointWith) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_owl_intersectionOf) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_owl_unionOf) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf__1) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf__2) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf__3) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_first) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_object) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_rest) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_subject) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_type) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_value) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_domain) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_isDefinedBy) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_member) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_range) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_seeAlso) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_subClassOf) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_subPropertyOf) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_ex_d) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_Alt) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_Bag) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_Property) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_XMLLiteral) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Class) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Container) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_ContainerMembershipProperty) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Datatype) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Literal) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_124) true
% 0.83/1.06       (icext $_124 uri_rdfs_Seq) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_124)
% 0.83/1.06       true (icext $_124 uri_rdf__1) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_124)
% 0.83/1.06       true (icext $_124 uri_rdf__2) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_124)
% 0.83/1.06       true (icext $_124 uri_rdf__3) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_124) true
% 0.83/1.06       (icext $_124 uri_rdf_XMLLiteral) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_124) true
% 0.83/1.06       (icext $_124 $_125) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06          $_187) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06          $_187) true (iext uri_rdfs_subClassOf uri_ex_d $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_ex_d $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_Alt $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_Alt $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_Bag $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_Bag $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_Property $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Class $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Container $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_187)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_187)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Literal $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_187) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_187) true
% 0.83/1.06       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_187) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.83/1.06       true (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_ex_d) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_ex_d) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_Alt) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Container) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_Alt) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_Bag) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Container) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_Bag) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_Property) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_XMLLiteral) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Literal) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdf_XMLLiteral) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Class) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Container) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.06       true (iext uri_rdfs_subClassOf $_185 uri_rdf_Property) true = true
% 0.83/1.06  |- ifeq
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.06       true (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Datatype) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Class) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Datatype) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Literal) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Seq) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Container) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_subClassOf $_185 uri_rdfs_Seq) true
% 0.83/1.06       (iext uri_rdfs_subClassOf $_185 uri_rdfs_Resource) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_List) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_nil $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_owl_complementOf $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_owl_disjointWith $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_owl_intersectionOf $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_owl_unionOf $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf__1 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf__2 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf__3 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_first $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_object $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_rest $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_subject $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_type $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_value $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_domain $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_isDefinedBy $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_member $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_range $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_seeAlso $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_subClassOf $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdf_Property) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_subPropertyOf $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq
% 0.83/1.06          (iext $_255
% 0.83/1.06             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.83/1.06             $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_ex_d $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_Alt $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_Bag $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_Property $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_XMLLiteral $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Class $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Container $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_ContainerMembershipProperty $_257) true
% 0.83/1.06          true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Datatype $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Literal $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Resource $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Class) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdfs_Seq $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.06       true (ifeq (iext $_255 uri_rdf__1 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.06       true (ifeq (iext $_255 uri_rdf__2 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_ContainerMembershipProperty)
% 0.83/1.06       true (ifeq (iext $_255 uri_rdf__3 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Datatype) true
% 0.83/1.06       (ifeq (iext $_255 uri_rdf_XMLLiteral $_257) true true true) true =
% 0.83/1.06     true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain $_255 uri_rdfs_Resource) true
% 0.83/1.06       (ifeq (iext $_255 $_256 $_257) true true true) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_owl_complementOf $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_owl_disjointWith $_254) true
% 0.83/1.06       (icext $_254 uri_ex_d) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_owl_intersectionOf $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_owl_unionOf $_254) true
% 0.83/1.06       (icext $_254 uri_ex_c) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_254) true
% 0.83/1.06       (icext $_254
% 0.83/1.06          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdf_type $_254) true (icext $_254 $_256)
% 0.83/1.06       true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.83/1.06       (icext $_254 uri_rdf__1) true = true
% 0.83/1.06  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.83/1.06       (icext $_254 uri_rdf__2) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__3) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_first) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_object) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_predicate) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_rest) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_subject) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_type) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_value) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_comment) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_domain) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_isDefinedBy) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_label) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_member) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_range) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_seeAlso) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subClassOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subPropertyOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__1) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__2) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__3) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_first) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_predicate) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_rest) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_subject) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_type) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_value) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_comment) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_domain) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_isDefinedBy) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_label) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_member) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_range) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_seeAlso) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subClassOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subPropertyOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254
% 0.90/1.07          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_ex_d) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_Alt) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_Bag) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_Property) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_XMLLiteral) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Class) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Container) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_ContainerMembershipProperty) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Datatype) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Literal) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Resource) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_Seq) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_owl_complementOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_owl_disjointWith) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_owl_intersectionOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_owl_unionOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__1) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__2) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf__3) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_first) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_object) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_rest) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_subject) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_type) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdf_value) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_domain) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_isDefinedBy) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_member) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_range) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_seeAlso) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subClassOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_254) true
% 0.90/1.07       (icext $_254 uri_rdfs_subPropertyOf) true = true
% 0.90/1.07  |- ifeq (iext uri_rdf_first $_256 $_257) true (icext uri_rdf_List $_256)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdf_object $_256 $_257) true
% 0.90/1.07       (icext uri_rdfs_Statement $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdf_predicate $_256 $_257) true
% 0.90/1.07       (icext uri_rdfs_Statement $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdf_rest $_256 $_257) true (icext uri_rdf_List $_256)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdf_subject $_256 $_257) true
% 0.90/1.07       (icext uri_rdfs_Statement $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_comment $_256 $_257) true true true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $_256 $_257) true
% 0.90/1.07       (icext uri_rdf_Property $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_label $_256 $_257) true true true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_256 $_257) true
% 0.90/1.07       (icext uri_rdf_Property $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf $_256 $_257) true
% 0.90/1.07       (icext uri_rdfs_Class $_256) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subPropertyOf $_256 $_257) true
% 0.90/1.07       (icext uri_rdf_Property $_256) true = true
% 0.90/1.07  |- icext uri_rdf_List
% 0.90/1.07       sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3 =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $P
% 0.90/1.07             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.07             $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.90/1.07       (icext $D
% 0.90/1.07          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.90/1.07       true = true
% 0.90/1.07  |- iext uri_rdf_type
% 0.90/1.07       sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.07       uri_rdf_List = true
% 0.90/1.07  |- icext uri_rdf_List
% 0.90/1.07       sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1 =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $P
% 0.90/1.07             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.07             $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.90/1.07       (icext $D
% 0.90/1.07          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.90/1.07       true = true
% 0.90/1.07  |- iext uri_rdf_type
% 0.90/1.07       sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.07       uri_rdf_List = true
% 0.90/1.07  |- icext uri_rdf_List
% 0.90/1.07       sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2 =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $P
% 0.90/1.07             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.07             $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.90/1.07       (icext $D
% 0.90/1.07          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.90/1.07       true = true
% 0.90/1.07  |- iext uri_rdf_type
% 0.90/1.07       sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.07       uri_rdf_List = true
% 0.90/1.07  |- icext uri_rdf_List
% 0.90/1.07       sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2 =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $P
% 0.90/1.07             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.07             $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.90/1.07       (icext $D
% 0.90/1.07          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.90/1.07       true = true
% 0.90/1.07  |- iext uri_rdf_type
% 0.90/1.07       sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.07       uri_rdf_List = true
% 0.90/1.07  |- icext uri_rdf_List
% 0.90/1.07       sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1 =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $P
% 0.90/1.07             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.07             $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.90/1.07       (icext $D
% 0.90/1.07          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.90/1.07       true = true
% 0.90/1.07  |- iext uri_rdf_type
% 0.90/1.07       sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.07       uri_rdf_List = true
% 0.90/1.07  |- icext uri_rdf_Property uri_rdf_predicate = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.90/1.07       (icext $D uri_rdf_predicate) true = true
% 0.90/1.07  |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true
% 0.90/1.07  |- ip uri_rdf_predicate = true
% 0.90/1.07  |- ifeq (iext uri_rdf_predicate $S $O) true true true = true
% 0.90/1.07  |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.90/1.07       (icext $C uri_rdf_predicate) true = true
% 0.90/1.07  |- icext uri_rdf_Property uri_rdfs_comment = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.90/1.07       (icext $D uri_rdfs_comment) true = true
% 0.90/1.07  |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true
% 0.90/1.07  |- ip uri_rdfs_comment = true
% 0.90/1.07  |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.90/1.07       (icext $C uri_rdfs_comment) true = true
% 0.90/1.07  |- icext uri_rdf_Property uri_rdfs_label = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.90/1.07       (icext $D uri_rdfs_label) true = true
% 0.90/1.07  |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true
% 0.90/1.07  |- ip uri_rdfs_label = true
% 0.90/1.07  |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.90/1.07       (icext $C uri_rdfs_label) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_List) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_nil) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_owl_complementOf) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_owl_disjointWith) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_owl_intersectionOf) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_owl_unionOf) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf__1) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf__2) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf__3) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_first) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_object) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_predicate) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_rest) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_subject) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_type) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_value) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_comment) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_domain) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_isDefinedBy) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_label) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_member) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_range) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_seeAlso) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_subClassOf) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdf_Property) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_subPropertyOf) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq
% 0.90/1.07          (iext $_380 $_381
% 0.90/1.07             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.07          true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_ex_d) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_Alt) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_Bag) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_Property) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_XMLLiteral) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Class) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Container) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_ContainerMembershipProperty) true
% 0.90/1.07          true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Datatype) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Literal) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Resource) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Class) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdfs_Seq) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.07       true (ifeq (iext $_380 $_381 uri_rdf__1) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.07       true (ifeq (iext $_380 $_381 uri_rdf__2) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.07       true (ifeq (iext $_380 $_381 uri_rdf__3) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Datatype) true
% 0.90/1.07       (ifeq (iext $_380 $_381 uri_rdf_XMLLiteral) true true true) true =
% 0.90/1.07     true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range $_380 uri_rdfs_Resource) true
% 0.90/1.07       (ifeq (iext $_380 $_381 $_382) true true true) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_owl_complementOf $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c2) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_owl_disjointWith $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c1) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_owl_intersectionOf $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_owl_unionOf $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_first $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c3) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_first $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c1) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_first $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c2) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_first $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_first $_379) true
% 0.90/1.07       (icext $_379 uri_ex_c) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_379) true
% 0.90/1.07       (icext $_379 uri_rdf_nil) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_379) true
% 0.90/1.07       (icext $_379
% 0.90/1.07          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.90/1.07       true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.07       (icext $_379 uri_rdf_List) true = true
% 0.90/1.07  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.07       (icext $_379 uri_rdfs_Class) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Property) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Datatype) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_ContainerMembershipProperty) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdf_type $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_List) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Statement) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Property) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Class) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_List) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Class) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Literal) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Property) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379
% 0.90/1.08          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_ex_d) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Alt) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Container) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Bag) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_Property) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_XMLLiteral) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Literal) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Class) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_ContainerMembershipProperty) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Datatype) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_Seq) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_owl_complementOf) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_owl_disjointWith) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_owl_intersectionOf) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_owl_unionOf) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf__1) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_member) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf__2) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf__3) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_first) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_object) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_predicate) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_rest) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_subject) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_type) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdf_value) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_comment) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_domain) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_isDefinedBy) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_seeAlso) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_label) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_range) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_subClassOf) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_379) true
% 0.90/1.08       (icext $_379 uri_rdfs_subPropertyOf) true = true
% 0.90/1.08  |- ifeq (iext uri_rdf_rest $_381 $_382) true (icext uri_rdf_List $_382)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdf_type $_381 $_382) true (icext uri_rdfs_Class $_382)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_comment $_381 $_382) true
% 0.90/1.08       (icext uri_rdfs_Literal $_382) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_domain $_381 $_382) true
% 0.90/1.08       (icext uri_rdfs_Class $_382) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_label $_381 $_382) true
% 0.90/1.08       (icext uri_rdfs_Literal $_382) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range $_381 $_382) true (icext uri_rdfs_Class $_382)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf $_381 $_382) true
% 0.90/1.08       (icext uri_rdfs_Class $_382) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_381 $_382) true
% 0.90/1.08       (icext uri_rdf_Property $_382) true = true
% 0.90/1.08  |- icext uri_rdfs_Class uri_rdf_List = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.90/1.08       (ifeq (iext $P $X uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.90/1.08       (ifeq (iext $P uri_rdf_List $Y) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.90/1.08       (icext $D uri_rdf_List) true = true
% 0.90/1.08  |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true
% 0.90/1.08  |- ic uri_rdf_List = true
% 0.90/1.08  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true
% 0.90/1.08  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.90/1.08       (icext $C uri_rdf_List) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.90/1.08       (icext $C uri_rdf_List) true = true
% 0.90/1.08  |- ifeq (icext uri_rdf_List $X) true (icext uri_rdf_List $X) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true
% 0.90/1.08       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.90/1.08       (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true
% 0.90/1.08  |- icext uri_rdfs_Class uri_rdfs_Statement = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.90/1.08       (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.90/1.08       (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.90/1.08       (icext $D uri_rdfs_Statement) true = true
% 0.90/1.08  |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true
% 0.90/1.08  |- ic uri_rdfs_Statement = true
% 0.90/1.08  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true
% 0.90/1.08  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.90/1.08       (icext $C uri_rdfs_Statement) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.90/1.08       (icext $C uri_rdfs_Statement) true = true
% 0.90/1.08  |- ifeq (icext uri_rdfs_Statement $X) true (icext uri_rdfs_Statement $X)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true
% 0.90/1.08       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.90/1.08       (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_owl_complementOf) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc
% 0.90/1.08             uri_ex_c2) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_owl_disjointWith) true
% 0.90/1.08       (ifeq (iext $_480 uri_ex_d uri_ex_c1) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_owl_intersectionOf) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.08             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_owl_unionOf) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480 uri_ex_c
% 0.90/1.08             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_first) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.08             uri_ex_c3) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_first) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.08             uri_ex_c1) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_first) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.08             uri_ex_c2) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_first) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.08             sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_first) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.08             uri_ex_c) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_rest) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.08             uri_rdf_nil) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_rest) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.08             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_rest) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.08             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_rest) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.08             uri_rdf_nil) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_rest) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.08             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.08             uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.08             uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.08             uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.08             uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.08             uri_rdfs_Class) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq
% 0.90/1.08          (iext $_480
% 0.90/1.08             sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.08             uri_rdf_List) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_ex_d uri_rdfs_Class) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_owl_complementOf uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_owl_disjointWith uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_owl_intersectionOf uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_owl_unionOf uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_Alt uri_rdfs_Class) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_Bag uri_rdfs_Class) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_List uri_rdfs_Class) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_Property uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_XMLLiteral uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__1 uri_rdf_Property) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__1 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__2 uri_rdf_Property) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__2 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__3 uri_rdf_Property) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__3 uri_rdfs_ContainerMembershipProperty)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_first uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_nil uri_rdf_List) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_object uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_predicate uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_rest uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_subject uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_type uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_value uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Container uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.90/1.08          true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Literal uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Resource uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Seq uri_rdfs_Class) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_Statement uri_rdfs_Class) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_comment uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_isDefinedBy uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_label uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_member uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_range uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_seeAlso uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_subClassOf uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdf_type) true
% 0.90/1.08       (ifeq (iext $_480 $_482 uri_rdfs_Resource) true true true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_first uri_rdf_List) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_object uri_rdfs_Statement) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_predicate uri_rdfs_Statement) true true
% 0.90/1.08          true) true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.90/1.08     true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_subject uri_rdfs_Statement) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_type uri_rdfs_Resource) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_comment uri_rdfs_Resource) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.90/1.08       true = true
% 0.90/1.08  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.08       (ifeq (iext $_480 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.90/1.08          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_label uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_range uri_rdf_Property) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_domain) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_first uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_predicate uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_subject uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_type uri_rdfs_Class) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_comment uri_rdfs_Literal) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_domain uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_label uri_rdfs_Literal) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_range uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_range) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480
% 0.90/1.09             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.09             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.09          true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480
% 0.90/1.09             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.09             uri_rdfs_Resource) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480 uri_ex_d
% 0.90/1.09             sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.09          true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_ex_d uri_ex_d) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_ex_d uri_rdfs_Resource) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Alt uri_rdf_Alt) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Alt uri_rdfs_Container) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Alt uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Bag uri_rdf_Bag) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Bag uri_rdfs_Container) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Bag uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_List uri_rdf_List) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_List uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Property uri_rdf_Property) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_Property uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_XMLLiteral uri_rdfs_Resource) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Class uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Container uri_rdfs_Container) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Container uri_rdfs_Resource) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.90/1.09          true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480 uri_rdfs_ContainerMembershipProperty
% 0.90/1.09             uri_rdfs_ContainerMembershipProperty) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq
% 0.90/1.09          (iext $_480 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.90/1.09          true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Datatype uri_rdfs_Datatype) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Datatype uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Literal uri_rdfs_Literal) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Literal uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Resource uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Seq uri_rdfs_Container) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Seq uri_rdfs_Resource) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Seq uri_rdfs_Seq) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Statement uri_rdfs_Resource) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subClassOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_Statement uri_rdfs_Statement) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_owl_complementOf uri_owl_complementOf) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_owl_disjointWith uri_owl_disjointWith) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_owl_intersectionOf uri_owl_intersectionOf) true
% 0.90/1.09          true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_owl_unionOf uri_owl_unionOf) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__1 uri_rdf__1) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__1 uri_rdfs_member) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__2 uri_rdf__2) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__2 uri_rdfs_member) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__3 uri_rdf__3) true true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf__3 uri_rdfs_member) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_first uri_rdf_first) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_object uri_rdf_object) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_predicate uri_rdf_predicate) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_rest uri_rdf_rest) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_subject uri_rdf_subject) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_type uri_rdf_type) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdf_value uri_rdf_value) true true true) true =
% 0.90/1.09     true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_comment uri_rdfs_comment) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_domain uri_rdfs_domain) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_label uri_rdfs_label) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_member uri_rdfs_member) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_range uri_rdfs_range) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true
% 0.90/1.09          true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf $_480 uri_rdfs_subPropertyOf) true
% 0.90/1.09       (ifeq (iext $_480 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true
% 0.90/1.09          true true) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_complementOf $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc
% 0.90/1.09          uri_ex_c2) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_disjointWith $_481) true
% 0.90/1.09       (iext $_481 uri_ex_d uri_ex_c1) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_intersectionOf $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.09          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_unionOf $_481) true
% 0.90/1.09       (iext $_481 uri_ex_c
% 0.90/1.09          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.09          uri_ex_c3) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.09          uri_ex_c1) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.09          uri_ex_c2) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.09          sK4_testcase_premise_fullish_020_Logical_Complications_BNODE_xc)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.09          uri_ex_c) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.09          uri_rdf_nil) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.09          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.09          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.09          uri_rdf_nil) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.09          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2)
% 0.90/1.09       true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK1_testcase_premise_fullish_020_Logical_Complications_BNODE_lu3
% 0.90/1.09          uri_rdf_List) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK2_testcase_premise_fullish_020_Logical_Complications_BNODE_lu1
% 0.90/1.09          uri_rdf_List) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK3_testcase_premise_fullish_020_Logical_Complications_BNODE_lu2
% 0.90/1.09          uri_rdf_List) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK5_testcase_premise_fullish_020_Logical_Complications_BNODE_li2
% 0.90/1.09          uri_rdf_List) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.09          uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481
% 0.90/1.09          sK7_testcase_premise_fullish_020_Logical_Complications_BNODE_li1
% 0.90/1.09          uri_rdf_List) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_ex_d uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_owl_complementOf uri_rdf_Property) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_owl_disjointWith uri_rdf_Property) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_owl_intersectionOf uri_rdf_Property) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_owl_unionOf uri_rdf_Property) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_rdf_Alt uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_rdf_Bag uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_rdf_List uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_rdf_Property uri_rdfs_Class) true = true
% 0.90/1.09  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.09       (iext $_481 uri_rdf_XMLLiteral uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true =
% 0.90/1.10     true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true =
% 0.90/1.10     true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true =
% 0.90/1.10     true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_first uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_nil uri_rdf_List) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_object uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_predicate uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_rest uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_subject uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_type uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_value uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Container uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Literal uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Resource uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Seq uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Statement uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_comment uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_domain uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_isDefinedBy uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_label uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_member uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_range uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_seeAlso uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subClassOf uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_481) true
% 0.90/1.10       (iext $_481 $_482 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_first uri_rdf_List) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_object uri_rdfs_Statement) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_predicate uri_rdfs_Statement) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_rest uri_rdf_List) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_subject uri_rdfs_Statement) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_type uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_value uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_comment uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_domain uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_label uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_range uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_first uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_predicate uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_rest uri_rdf_List) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_subject uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_type uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_value uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_comment uri_rdfs_Literal) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_domain uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_label uri_rdfs_Literal) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_range uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481
% 0.90/1.10          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.10          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481
% 0.90/1.10          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs
% 0.90/1.10          uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_ex_d
% 0.90/1.10          sK6_testcase_premise_fullish_020_Logical_Complications_BNODE_xs)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_ex_d uri_ex_d) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_ex_d uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Alt uri_rdf_Alt) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Alt uri_rdfs_Container) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Alt uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Bag uri_rdf_Bag) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Bag uri_rdfs_Container) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Bag uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_List uri_rdf_List) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_List uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Property uri_rdf_Property) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_Property uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Class uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Container uri_rdfs_Container) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Container uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_ContainerMembershipProperty
% 0.90/1.10          uri_rdfs_ContainerMembershipProperty) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Datatype uri_rdfs_Datatype) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Datatype uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Literal uri_rdfs_Literal) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Literal uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Resource uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Seq uri_rdfs_Container) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Seq uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Seq uri_rdfs_Seq) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Statement uri_rdfs_Resource) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_Statement uri_rdfs_Statement) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_owl_complementOf uri_owl_complementOf) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_owl_disjointWith uri_owl_disjointWith) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_owl_intersectionOf uri_owl_intersectionOf) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_owl_unionOf uri_owl_unionOf) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdf__1) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__1 uri_rdfs_member) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdf__2) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__2 uri_rdfs_member) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdf__3) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf__3 uri_rdfs_member) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_first uri_rdf_first) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_object uri_rdf_object) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_predicate uri_rdf_predicate) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_rest uri_rdf_rest) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_subject uri_rdf_subject) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_type uri_rdf_type) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdf_value uri_rdf_value) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_comment uri_rdfs_comment) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_domain uri_rdfs_domain) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_label uri_rdfs_label) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_member uri_rdfs_member) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_range uri_rdfs_range) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_481) true
% 0.90/1.10       (iext $_481 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true
% 0.90/1.10  |- ifeq (iext uri_owl_complementOf $_482 $_483) true
% 0.90/1.10       (iext uri_owl_complementOf $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_owl_disjointWith $_482 $_483) true
% 0.90/1.10       (iext uri_owl_disjointWith $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_owl_intersectionOf $_482 $_483) true
% 0.90/1.10       (iext uri_owl_intersectionOf $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_owl_unionOf $_482 $_483) true
% 0.90/1.10       (iext uri_owl_unionOf $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__1 $_482 $_483) true (iext uri_rdf__1 $_482 $_483)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__1 $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_member $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__2 $_482 $_483) true (iext uri_rdf__2 $_482 $_483)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__2 $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_member $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__3 $_482 $_483) true (iext uri_rdf__3 $_482 $_483)
% 0.90/1.10       true = true
% 0.90/1.10  |- ifeq (iext uri_rdf__3 $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_member $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_first $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_first $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_object $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_object $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_predicate $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_predicate $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_rest $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_rest $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_subject $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_subject $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_type $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_type $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdf_value $_482 $_483) true
% 0.90/1.10       (iext uri_rdf_value $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_comment $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_comment $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_domain $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_domain $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_isDefinedBy $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_isDefinedBy $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_isDefinedBy $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_seeAlso $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_label $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_label $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_member $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_member $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_range $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_range $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_seeAlso $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_seeAlso $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subClassOf $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_subClassOf $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf $_482 $_483) true
% 0.90/1.10       (iext uri_rdfs_subPropertyOf $_482 $_483) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_1066) true
% 0.90/1.10       (iext uri_rdfs_subPropertyOf uri_rdf__1 $_1066) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_1066) true
% 0.90/1.10       (iext uri_rdfs_subPropertyOf uri_rdf__2 $_1066) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_1066) true
% 0.90/1.10       (iext uri_rdfs_subPropertyOf uri_rdf__3 $_1066) true = true
% 0.90/1.10  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_1066) true
% 0.90/1.10       (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_1066) true = true
% 0.90/1.11  |- ifeq (iext uri_rdfs_subPropertyOf $_1064 uri_rdf__1) true
% 0.90/1.11       (iext uri_rdfs_subPropertyOf $_1064 uri_rdfs_member) true = true
% 0.90/1.11  |- ifeq (iext uri_rdfs_subPropertyOf $_1064 uri_rdf__2) true
% 0.90/1.11       (iext uri_rdfs_subPropertyOf $_1064 uri_rdfs_member) true = true
% 0.90/1.11  |- ifeq (iext uri_rdfs_subPropertyOf $_1064 uri_rdf__3) true
% 0.90/1.11       (iext uri_rdfs_subPropertyOf $_1064 uri_rdfs_member) true = true
% 0.90/1.11  |- ifeq (iext uri_rdfs_subPropertyOf $_1064 uri_rdfs_isDefinedBy) true
% 0.90/1.11       (iext uri_rdfs_subPropertyOf $_1064 uri_rdfs_seeAlso) true = true
% 0.90/1.11  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.90/1.11  
%------------------------------------------------------------------------------