Metis---2.4.SAT-Sat.s

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

% Computer : n020.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:20 EDT 2022

% Result   : Satisfiable 0.99s 1.15s
% Output   : Saturation 1.08s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB013-10 : TPTP v8.1.0. Released v7.3.0.
% 0.07/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n020.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 00:38:23 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.99/1.15  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.99/1.15  
% 0.99/1.15  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.99/1.15  |- ifeq $A $A $B $C = $B
% 0.99/1.15  |- ifeq (iext $P $S $O) true (ip $P) true = true
% 0.99/1.15  |- ir $X = true
% 0.99/1.15  |- ifeq (lv $X) true true true = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true
% 0.99/1.15  |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true
% 0.99/1.15  |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true
% 0.99/1.15  |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true
% 0.99/1.16  |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true
% 0.99/1.16  |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true
% 0.99/1.16  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true =
% 0.99/1.16     true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true
% 0.99/1.16  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true
% 0.99/1.16       (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.99/1.16       uri_rdf_Property = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.16  |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.16  |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true
% 0.99/1.16  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true
% 0.99/1.16  |- ifeq (icext uri_rdfs_Datatype $D) true
% 0.99/1.16       (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_domain $P $C) true
% 0.99/1.16       (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true
% 0.99/1.16  |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true
% 0.99/1.16  |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true
% 0.99/1.16  |- icext uri_rdfs_Resource $X = true
% 0.99/1.16  |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true
% 0.99/1.16  |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true
% 0.99/1.16  |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_range $P $C) true
% 0.99/1.16       (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.99/1.16  |- ifeq (icext $C $X) true
% 0.99/1.16       (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true =
% 0.99/1.16     true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true
% 0.99/1.16  |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subClassOf $D $E) true
% 0.99/1.16       (ifeq (iext uri_rdfs_subClassOf $C $D) true
% 0.99/1.16          (iext uri_rdfs_subClassOf $C $E) true) true = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.99/1.16       (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.99/1.16  |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true
% 0.99/1.16  |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true
% 0.99/1.16       (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true
% 0.99/1.16          (iext uri_rdfs_subPropertyOf $P $R) true) true = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true
% 0.99/1.16  |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true
% 0.99/1.16  |- iext uri_owl_inverseOf sK3_testcase_premise_fullish_013_Cliques_BNODE_i
% 0.99/1.16       uri_rdf_type = true
% 0.99/1.16  |- iext uri_owl_propertyChainAxiom uri_foaf_knows
% 0.99/1.16       sK1_testcase_premise_fullish_013_Cliques_BNODE_l1 = true
% 0.99/1.16  |- iext uri_owl_someValuesFrom
% 0.99/1.16       sK5_testcase_premise_fullish_013_Cliques_BNODE_r uri_ex_Clique = true
% 0.99/1.16  |- iext uri_owl_onProperty sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.16       uri_ex_sameCliqueAs = true
% 0.99/1.16  |- iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique = true
% 0.99/1.16  |- iext uri_rdf_rest sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.16       sK2_testcase_premise_fullish_013_Cliques_BNODE_l2 = true
% 0.99/1.16  |- iext uri_rdf_rest sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.16       sK4_testcase_premise_fullish_013_Cliques_BNODE_l3 = true
% 0.99/1.16  |- iext uri_rdf_rest sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.16       uri_rdf_nil = true
% 0.99/1.16  |- iext uri_rdf_first sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.16       uri_rdf_type = true
% 0.99/1.16  |- iext uri_rdf_first sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.16       uri_ex_sameCliqueAs = true
% 0.99/1.16  |- iext uri_rdf_first sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.16       sK3_testcase_premise_fullish_013_Cliques_BNODE_i = true
% 0.99/1.16  |- iext uri_rdf_type sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.16       uri_owl_Restriction = true
% 0.99/1.16  |- iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique = true
% 0.99/1.16  |- iext uri_rdf_type uri_ex_Clique uri_owl_Class = true
% 0.99/1.16  |- iext uri_rdf_type uri_ex_bob uri_ex_JoesGang = true
% 0.99/1.16  |- iext uri_rdf_type uri_ex_alice uri_ex_JoesGang = true
% 0.99/1.16  |- iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_ex_Clique
% 0.99/1.16       sK5_testcase_premise_fullish_013_Cliques_BNODE_r = true
% 0.99/1.16  |- ~(iext uri_foaf_knows uri_ex_alice uri_ex_bob = true)
% 0.99/1.16  |- ip uri_rdf__1 = true
% 0.99/1.16  |- ip uri_rdf__2 = true
% 0.99/1.16  |- ip uri_rdf__3 = true
% 0.99/1.16  |- ip uri_rdf_first = true
% 0.99/1.16  |- ip uri_rdf_object = true
% 0.99/1.16  |- ip uri_rdf_rest = true
% 0.99/1.16  |- ip uri_rdf_subject = true
% 0.99/1.16  |- ip uri_rdf_type = true
% 0.99/1.16  |- ip uri_rdf_value = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true
% 0.99/1.16  |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true
% 0.99/1.16  |- ic sK5_testcase_premise_fullish_013_Cliques_BNODE_r = true
% 0.99/1.16  |- ic uri_rdfs_Container = true
% 0.99/1.16  |- ic uri_rdfs_Literal = true
% 0.99/1.16  |- ic uri_rdf_Property = true
% 0.99/1.16  |- ic uri_rdfs_Class = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf
% 0.99/1.16       sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.16       sK5_testcase_premise_fullish_013_Cliques_BNODE_r = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf
% 0.99/1.16       sK5_testcase_premise_fullish_013_Cliques_BNODE_r uri_rdfs_Resource =
% 0.99/1.16     true
% 0.99/1.16  |- icext uri_rdfs_Class sK5_testcase_premise_fullish_013_Cliques_BNODE_r =
% 0.99/1.16     true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true
% 0.99/1.16  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true
% 0.99/1.16  |- icext uri_rdfs_Class uri_rdfs_Container = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_Literal = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdf_Property = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_Class = true
% 0.99/1.17  |- ic uri_rdfs_Resource = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_Resource = true
% 0.99/1.17  |- ip uri_ex_sameCliqueAs = true
% 0.99/1.17  |- ip uri_rdfs_isDefinedBy = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_ex_sameCliqueAs =
% 0.99/1.17     true
% 0.99/1.17  |- iext uri_rdf_type uri_ex_sameCliqueAs uri_rdf_Property = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy =
% 0.99/1.17     true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true
% 0.99/1.17  |- ic uri_ex_Clique = true
% 0.99/1.17  |- ic uri_rdf_Alt = true
% 0.99/1.17  |- ic uri_rdf_Bag = true
% 0.99/1.17  |- ic uri_rdf_XMLLiteral = true
% 0.99/1.17  |- ic uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.17  |- ic uri_rdfs_Datatype = true
% 0.99/1.17  |- ic uri_rdfs_Seq = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_ex_Clique uri_ex_Clique = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_ex_Clique uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_ex_Clique = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdf_Alt = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdf_Bag = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.99/1.17       uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.99/1.17       uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_Datatype = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true
% 0.99/1.17  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_rdfs_Class uri_rdfs_Seq = true
% 0.99/1.17  |- ip uri_owl_sameAs = true
% 0.99/1.17  |- ip uri_rdfs_seeAlso = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_owl_sameAs uri_owl_sameAs = true
% 0.99/1.17  |- iext uri_rdf_type uri_owl_sameAs uri_rdf_Property = true
% 0.99/1.17  |- iext uri_rdf_type sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.17       uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_ex_Clique uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class =
% 0.99/1.17     true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true
% 0.99/1.17  |- iext uri_rdf_type $_57 uri_rdfs_Resource = true
% 0.99/1.17  |- icext uri_owl_Restriction
% 0.99/1.17       sK5_testcase_premise_fullish_013_Cliques_BNODE_r = true
% 0.99/1.17  |- icext uri_owl_Class uri_ex_Clique = true
% 0.99/1.17  |- icext uri_ex_Clique uri_ex_JoesGang = true
% 0.99/1.17  |- icext uri_ex_JoesGang uri_ex_alice = true
% 0.99/1.17  |- icext uri_ex_JoesGang uri_ex_bob = true
% 0.99/1.17  |- icext uri_rdf_Property uri_ex_sameCliqueAs = true
% 0.99/1.17  |- icext uri_owl_ObjectProperty uri_foaf_knows = true
% 0.99/1.17  |- icext uri_rdf_Property uri_owl_sameAs = true
% 0.99/1.17  |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf__1 = true
% 0.99/1.17  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf__2 = true
% 0.99/1.17  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf__3 = true
% 0.99/1.17  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_first = true
% 0.99/1.17  |- icext uri_rdf_List uri_rdf_nil = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_object = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_rest = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_subject = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_type = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdf_value = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_seeAlso = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true
% 0.99/1.17  |- ip uri_rdfs_member = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_member = true
% 0.99/1.17  |- ifeq (iext uri_ex_sameCliqueAs $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_owl_sameAs $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf__1 $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf__2 $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf__3 $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_first $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_object $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_rest $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_subject $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_type $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdf_value $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_isDefinedBy $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_member $_86 $_84) true true true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_seeAlso $_86 $_84) true true true = true
% 0.99/1.17  |- ip uri_owl_inverseOf = true
% 0.99/1.17  |- ip uri_owl_onProperty = true
% 0.99/1.17  |- ip uri_owl_propertyChainAxiom = true
% 0.99/1.17  |- ip uri_owl_someValuesFrom = true
% 0.99/1.17  |- ip uri_rdfs_domain = true
% 0.99/1.17  |- ip uri_rdfs_range = true
% 0.99/1.17  |- ip uri_rdfs_subClassOf = true
% 0.99/1.17  |- ip uri_rdfs_subPropertyOf = true
% 0.99/1.17  |- ifeq (iext uri_owl_inverseOf $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_owl_inverseOf uri_owl_inverseOf = true
% 0.99/1.17  |- iext uri_rdf_type uri_owl_inverseOf uri_rdf_Property = true
% 0.99/1.17  |- ifeq (iext uri_owl_onProperty $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_owl_onProperty uri_owl_onProperty = true
% 0.99/1.17  |- iext uri_rdf_type uri_owl_onProperty uri_rdf_Property = true
% 0.99/1.17  |- ifeq (iext uri_owl_propertyChainAxiom $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_owl_propertyChainAxiom
% 0.99/1.17       uri_owl_propertyChainAxiom = true
% 0.99/1.17  |- iext uri_rdf_type uri_owl_propertyChainAxiom uri_rdf_Property = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_domain $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_owl_inverseOf = true
% 0.99/1.17  |- icext uri_rdf_Property uri_owl_onProperty = true
% 0.99/1.17  |- icext uri_rdf_Property uri_owl_propertyChainAxiom = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_domain = true
% 0.99/1.17  |- ifeq (iext uri_owl_someValuesFrom $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_owl_someValuesFrom
% 0.99/1.17       uri_owl_someValuesFrom = true
% 0.99/1.17  |- iext uri_rdf_type uri_owl_someValuesFrom uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_owl_someValuesFrom = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_range $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_range = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf =
% 0.99/1.17     true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_subClassOf = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true
% 0.99/1.17  |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.99/1.17       uri_rdfs_subPropertyOf = true
% 0.99/1.17  |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true
% 0.99/1.17  |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true
% 0.99/1.17  |- ifeq (icext $_131 $_133) true true true = true
% 0.99/1.17  |- ifeq (icext sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_133) true
% 0.99/1.17       (icext sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (icext uri_ex_Clique $_133) true
% 0.99/1.17       (icext sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (icext uri_ex_Clique $_133) true (icext uri_ex_Clique $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (icext uri_rdf_Alt $_133) true (icext uri_rdf_Alt $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (icext uri_rdf_Alt $_133) true (icext uri_rdfs_Container $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdf_Bag $_133) true (icext uri_rdf_Bag $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (icext uri_rdf_Bag $_133) true (icext uri_rdfs_Container $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdf_Property $_133) true (icext uri_rdf_Property $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdf_XMLLiteral $_133) true
% 0.99/1.17       (icext uri_rdf_XMLLiteral $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdf_XMLLiteral $_133) true
% 0.99/1.17       (icext uri_rdfs_Literal $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Class $_133) true (icext uri_rdfs_Class $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Container $_133) true
% 0.99/1.17       (icext uri_rdfs_Container $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_133) true
% 0.99/1.17       (icext uri_rdf_Property $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_133) true
% 0.99/1.17       (icext uri_rdfs_ContainerMembershipProperty $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Datatype $_133) true (icext uri_rdfs_Class $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Datatype $_133) true
% 0.99/1.17       (icext uri_rdfs_Datatype $_133) true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Literal $_133) true (icext uri_rdfs_Literal $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Seq $_133) true (icext uri_rdfs_Container $_133)
% 0.99/1.17       true = true
% 0.99/1.17  |- ifeq (icext uri_rdfs_Seq $_133) true (icext uri_rdfs_Seq $_133) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_ex_Clique $_132) true
% 0.99/1.17       (icext $_132 uri_ex_JoesGang) true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_ex_JoesGang $_132) true
% 0.99/1.17       (icext $_132 uri_ex_alice) true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_ex_JoesGang $_132) true
% 0.99/1.17       (icext $_132 uri_ex_bob) true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_owl_Class $_132) true
% 0.99/1.17       (icext $_132 uri_ex_Clique) true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_owl_ObjectProperty $_132) true
% 0.99/1.17       (icext $_132 uri_foaf_knows) true = true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_owl_Restriction $_132) true
% 0.99/1.17       (icext $_132 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.17     true
% 0.99/1.17  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_132) true
% 0.99/1.17       (icext $_132 uri_rdf_nil) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_ex_sameCliqueAs) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_owl_inverseOf) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_owl_onProperty) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_owl_propertyChainAxiom) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_owl_sameAs) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_owl_someValuesFrom) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf__1) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf__2) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf__3) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_first) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_object) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_rest) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_subject) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_type) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_value) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_domain) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_isDefinedBy) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_member) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_range) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_seeAlso) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_subClassOf) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_subPropertyOf) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_ex_Clique) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_Alt) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_Bag) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_Property) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_XMLLiteral) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Class) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Container) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_ContainerMembershipProperty) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Datatype) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Literal) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_132) true
% 0.99/1.18       (icext $_132 uri_rdfs_Seq) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_132)
% 0.99/1.18       true (icext $_132 uri_rdf__1) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_132)
% 0.99/1.18       true (icext $_132 uri_rdf__2) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_132)
% 0.99/1.18       true (icext $_132 uri_rdf__3) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_132) true
% 0.99/1.18       (icext $_132 uri_rdf_XMLLiteral) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_132) true
% 0.99/1.18       (icext $_132 $_133) true = true
% 0.99/1.18  |- icext sK5_testcase_premise_fullish_013_Cliques_BNODE_r uri_ex_JoesGang =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r $D) true
% 0.99/1.18       (icext $D uri_ex_JoesGang) true = true
% 0.99/1.18  |- iext uri_rdf_type uri_ex_JoesGang
% 0.99/1.18       sK5_testcase_premise_fullish_013_Cliques_BNODE_r = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_206) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_ex_Clique $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_ex_Clique $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_Alt $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_Alt $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_Bag $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_Bag $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_Property $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Class $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Container $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_206)
% 0.99/1.18       true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_206)
% 0.99/1.18       true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Literal $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_206) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_206) true
% 0.99/1.18       (iext uri_rdfs_subClassOf uri_rdfs_Seq $_206) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_ex_Clique) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_ex_Clique) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_Alt) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Container) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_Alt) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_Bag) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Container) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_Bag) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_Property) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_XMLLiteral) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Literal) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdf_XMLLiteral) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Class) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Container) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.18       true (iext uri_rdfs_subClassOf $_204 uri_rdf_Property) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.18       true (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Datatype) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Class) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Datatype) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Literal) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Seq) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Container) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subClassOf $_204 uri_rdfs_Seq) true
% 0.99/1.18       (iext uri_rdfs_subClassOf $_204 uri_rdfs_Resource) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_sameAs $_273) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs $_273) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_273) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf uri_rdf__1 $_273) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_273) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf uri_rdf__2 $_273) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_273) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf uri_rdf__3 $_273) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_273) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_273) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf $_271 uri_ex_sameCliqueAs) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf $_271 uri_owl_sameAs) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf $_271 uri_rdf__1) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf $_271 uri_rdfs_member) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf $_271 uri_rdf__2) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf $_271 uri_rdfs_member) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf $_271 uri_rdf__3) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf $_271 uri_rdfs_member) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_subPropertyOf $_271 uri_rdfs_isDefinedBy) true
% 0.99/1.18       (iext uri_rdfs_subPropertyOf $_271 uri_rdfs_seeAlso) true = true
% 0.99/1.18  |- ifeq
% 0.99/1.18       (iext uri_rdfs_domain $_329
% 0.99/1.18          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_JoesGang $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_ex_Clique) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_JoesGang $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_ex_JoesGang) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_alice $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_ex_JoesGang) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_bob $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_owl_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_Clique $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_owl_ObjectProperty) true
% 0.99/1.18       (ifeq (iext $_329 uri_foaf_knows $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_owl_Restriction) true
% 0.99/1.18       (ifeq
% 0.99/1.18          (iext $_329 sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_331)
% 0.99/1.18          true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_List) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_nil $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_sameCliqueAs $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_owl_inverseOf $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_owl_onProperty $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_owl_propertyChainAxiom $_331) true true true)
% 0.99/1.18       true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_owl_sameAs $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_owl_someValuesFrom $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf__1 $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf__2 $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf__3 $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_first $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_object $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_rest $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_subject $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_type $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_value $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_domain $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_isDefinedBy $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_member $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_range $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_seeAlso $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_subClassOf $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdf_Property) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_subPropertyOf $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq
% 0.99/1.18          (iext $_329 sK5_testcase_premise_fullish_013_Cliques_BNODE_r $_331)
% 0.99/1.18          true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_ex_Clique $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_Alt $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_Bag $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_Property $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdf_XMLLiteral $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Class $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Container $_331) true true true) true =
% 0.99/1.18     true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_ContainerMembershipProperty $_331) true
% 0.99/1.18          true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Datatype $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Literal $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Resource $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Class) true
% 0.99/1.18       (ifeq (iext $_329 uri_rdfs_Seq $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.18       true (ifeq (iext $_329 uri_rdf__1 $_331) true true true) true = true
% 0.99/1.18  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.18       true (ifeq (iext $_329 uri_rdf__2 $_331) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.19       true (ifeq (iext $_329 uri_rdf__3 $_331) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Datatype) true
% 0.99/1.19       (ifeq (iext $_329 uri_rdf_XMLLiteral $_331) true true true) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $_329 uri_rdfs_Resource) true
% 0.99/1.19       (ifeq (iext $_329 $_330 $_331) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_owl_inverseOf $_328) true
% 0.99/1.19       (icext $_328 sK3_testcase_premise_fullish_013_Cliques_BNODE_i) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_owl_onProperty $_328) true
% 0.99/1.19       (icext $_328 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_owl_propertyChainAxiom $_328) true
% 0.99/1.19       (icext $_328 uri_foaf_knows) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_owl_someValuesFrom $_328) true
% 0.99/1.19       (icext $_328 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_328) true
% 0.99/1.19       (icext $_328 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_328) true
% 0.99/1.19       (icext $_328 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_first $_328) true
% 0.99/1.19       (icext $_328 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_328) true
% 0.99/1.19       (icext $_328 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_328) true
% 0.99/1.19       (icext $_328 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_328) true
% 0.99/1.19       (icext $_328 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdf_type $_328) true (icext $_328 $_330)
% 0.99/1.19       true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__1) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__2) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__3) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_first) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_object) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_predicate) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_rest) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_subject) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_type) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_value) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_comment) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_domain) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_isDefinedBy) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_label) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_member) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_range) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_seeAlso) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subClassOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subPropertyOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_ex_sameCliqueAs) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__1) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__2) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__3) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_first) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_predicate) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_rest) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_subject) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_type) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_value) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_comment) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_domain) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_isDefinedBy) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_label) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_member) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_range) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_seeAlso) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subClassOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subPropertyOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_ex_Clique) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_Alt) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_Bag) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_Property) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_XMLLiteral) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Class) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Container) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_ContainerMembershipProperty) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Datatype) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Literal) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Resource) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_Seq) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_ex_sameCliqueAs) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_owl_inverseOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_owl_onProperty) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_owl_propertyChainAxiom) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_owl_sameAs) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_owl_someValuesFrom) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__1) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__2) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf__3) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_first) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_object) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_rest) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_subject) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_type) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdf_value) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_domain) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_isDefinedBy) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_member) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_range) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_seeAlso) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subClassOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_328) true
% 0.99/1.19       (icext $_328 uri_rdfs_subPropertyOf) true = true
% 0.99/1.19  |- ifeq (iext uri_rdf_first $_330 $_331) true (icext uri_rdf_List $_330)
% 0.99/1.19       true = true
% 0.99/1.19  |- ifeq (iext uri_rdf_object $_330 $_331) true
% 0.99/1.19       (icext uri_rdfs_Statement $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdf_predicate $_330 $_331) true
% 0.99/1.19       (icext uri_rdfs_Statement $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdf_rest $_330 $_331) true (icext uri_rdf_List $_330)
% 0.99/1.19       true = true
% 0.99/1.19  |- ifeq (iext uri_rdf_subject $_330 $_331) true
% 0.99/1.19       (icext uri_rdfs_Statement $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_comment $_330 $_331) true true true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $_330 $_331) true
% 0.99/1.19       (icext uri_rdf_Property $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_label $_330 $_331) true true true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_330 $_331) true
% 0.99/1.19       (icext uri_rdf_Property $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf $_330 $_331) true
% 0.99/1.19       (icext uri_rdfs_Class $_330) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subPropertyOf $_330 $_331) true
% 0.99/1.19       (icext uri_rdf_Property $_330) true = true
% 0.99/1.19  |- icext uri_rdf_List sK1_testcase_premise_fullish_013_Cliques_BNODE_l1 =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.99/1.19       (ifeq (iext $P sK1_testcase_premise_fullish_013_Cliques_BNODE_l1 $Y)
% 0.99/1.19          true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.99/1.19       (icext $D sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true =
% 0.99/1.19     true
% 0.99/1.19  |- iext uri_rdf_type sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.19       uri_rdf_List = true
% 0.99/1.19  |- icext uri_rdf_List sK2_testcase_premise_fullish_013_Cliques_BNODE_l2 =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.99/1.19       (ifeq (iext $P sK2_testcase_premise_fullish_013_Cliques_BNODE_l2 $Y)
% 0.99/1.19          true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.99/1.19       (icext $D sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true =
% 0.99/1.19     true
% 0.99/1.19  |- iext uri_rdf_type sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.19       uri_rdf_List = true
% 0.99/1.19  |- icext uri_rdf_List sK4_testcase_premise_fullish_013_Cliques_BNODE_l3 =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true
% 0.99/1.19       (ifeq (iext $P sK4_testcase_premise_fullish_013_Cliques_BNODE_l3 $Y)
% 0.99/1.19          true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true
% 0.99/1.19       (icext $D sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true =
% 0.99/1.19     true
% 0.99/1.19  |- iext uri_rdf_type sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.19       uri_rdf_List = true
% 0.99/1.19  |- icext uri_rdf_Property uri_rdf_predicate = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.99/1.19       (icext $D uri_rdf_predicate) true = true
% 0.99/1.19  |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true
% 0.99/1.19  |- ip uri_rdf_predicate = true
% 0.99/1.19  |- ifeq (iext uri_rdf_predicate $S $O) true true true = true
% 0.99/1.19  |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.99/1.19       (icext $C uri_rdf_predicate) true = true
% 0.99/1.19  |- icext uri_rdf_Property uri_rdfs_comment = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.99/1.19       (icext $D uri_rdfs_comment) true = true
% 0.99/1.19  |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true
% 0.99/1.19  |- ip uri_rdfs_comment = true
% 0.99/1.19  |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.99/1.19       (icext $C uri_rdfs_comment) true = true
% 0.99/1.19  |- icext uri_rdf_Property uri_rdfs_label = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true
% 0.99/1.19       (icext $D uri_rdfs_label) true = true
% 0.99/1.19  |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true
% 0.99/1.19  |- ip uri_rdfs_label = true
% 0.99/1.19  |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true
% 0.99/1.19       (icext $C uri_rdfs_label) true = true
% 0.99/1.19  |- ifeq
% 0.99/1.19       (iext uri_rdfs_range $_457
% 0.99/1.19          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_JoesGang) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_ex_Clique) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_JoesGang) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_ex_JoesGang) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_alice) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_ex_JoesGang) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_bob) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_owl_Class) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_Clique) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_owl_ObjectProperty) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_foaf_knows) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_owl_Restriction) true
% 0.99/1.19       (ifeq
% 0.99/1.19          (iext $_457 $_458 sK5_testcase_premise_fullish_013_Cliques_BNODE_r)
% 0.99/1.19          true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_List) true
% 0.99/1.19       (ifeq
% 0.99/1.19          (iext $_457 $_458
% 0.99/1.19             sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true true
% 0.99/1.19          true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_List) true
% 0.99/1.19       (ifeq
% 0.99/1.19          (iext $_457 $_458
% 0.99/1.19             sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true true
% 0.99/1.19          true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_List) true
% 0.99/1.19       (ifeq
% 0.99/1.19          (iext $_457 $_458
% 0.99/1.19             sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true true
% 0.99/1.19          true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_List) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_nil) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_ex_sameCliqueAs) true true true) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_owl_inverseOf) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_owl_onProperty) true true true) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_owl_propertyChainAxiom) true true true)
% 0.99/1.19       true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_owl_sameAs) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_owl_someValuesFrom) true true true) true =
% 0.99/1.19     true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf__1) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf__2) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf__3) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_first) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_object) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_predicate) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_rest) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_subject) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_type) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdf_value) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdfs_comment) true true true) true = true
% 0.99/1.19  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.19       (ifeq (iext $_457 $_458 uri_rdfs_domain) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_isDefinedBy) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_label) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_member) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_range) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_seeAlso) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_subClassOf) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdf_Property) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_subPropertyOf) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq
% 0.99/1.20          (iext $_457 $_458 sK5_testcase_premise_fullish_013_Cliques_BNODE_r)
% 0.99/1.20          true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_ex_Clique) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdf_Alt) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdf_Bag) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdf_Property) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdf_XMLLiteral) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Class) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Container) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_ContainerMembershipProperty) true
% 0.99/1.20          true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Datatype) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Literal) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Resource) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdfs_Seq) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.20       true (ifeq (iext $_457 $_458 uri_rdf__1) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.20       true (ifeq (iext $_457 $_458 uri_rdf__2) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.20       true (ifeq (iext $_457 $_458 uri_rdf__3) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Datatype) true
% 0.99/1.20       (ifeq (iext $_457 $_458 uri_rdf_XMLLiteral) true true true) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_457 uri_rdfs_Resource) true
% 0.99/1.20       (ifeq (iext $_457 $_458 $_459) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_owl_inverseOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_type) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_owl_onProperty $_456) true
% 0.99/1.20       (icext $_456 uri_ex_sameCliqueAs) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_owl_propertyChainAxiom $_456) true
% 0.99/1.20       (icext $_456 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_owl_someValuesFrom $_456) true
% 0.99/1.20       (icext $_456 uri_ex_Clique) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_first $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_type) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_first $_456) true
% 0.99/1.20       (icext $_456 uri_ex_sameCliqueAs) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_first $_456) true
% 0.99/1.20       (icext $_456 sK3_testcase_premise_fullish_013_Cliques_BNODE_i) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_456) true
% 0.99/1.20       (icext $_456 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_456) true
% 0.99/1.20       (icext $_456 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_rest $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_nil) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_List) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_owl_Restriction) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_owl_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_ex_Clique) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_ex_JoesGang) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Property) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_owl_ObjectProperty) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Datatype) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_ContainerMembershipProperty) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdf_type $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_List) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Statement) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Property) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_ex_Clique) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_List) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Literal) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_range $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Property) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_ex_Clique) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Alt) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Container) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Bag) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_Property) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_XMLLiteral) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Literal) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_ContainerMembershipProperty) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Datatype) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_Seq) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_ex_sameCliqueAs) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_owl_sameAs) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_owl_inverseOf) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_owl_onProperty) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_owl_propertyChainAxiom) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_owl_someValuesFrom) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf__1) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_member) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf__2) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf__3) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_first) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_object) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_predicate) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_rest) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_subject) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_type) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdf_value) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_comment) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_domain) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_isDefinedBy) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_seeAlso) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_label) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_range) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_subClassOf) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_456) true
% 0.99/1.20       (icext $_456 uri_rdfs_subPropertyOf) true = true
% 0.99/1.20  |- ifeq (iext uri_ex_sameCliqueAs $_458 $_459) true
% 0.99/1.20       (icext uri_ex_Clique $_459) true = true
% 0.99/1.20  |- ifeq (iext uri_rdf_rest $_458 $_459) true (icext uri_rdf_List $_459)
% 0.99/1.20       true = true
% 0.99/1.20  |- ifeq (iext uri_rdf_type $_458 $_459) true (icext uri_rdfs_Class $_459)
% 0.99/1.20       true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_comment $_458 $_459) true
% 0.99/1.20       (icext uri_rdfs_Literal $_459) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $_458 $_459) true
% 0.99/1.20       (icext uri_rdfs_Class $_459) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_label $_458 $_459) true
% 0.99/1.20       (icext uri_rdfs_Literal $_459) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $_458 $_459) true (icext uri_rdfs_Class $_459)
% 0.99/1.20       true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $_458 $_459) true
% 0.99/1.20       (icext uri_rdfs_Class $_459) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subPropertyOf $_458 $_459) true
% 0.99/1.20       (icext uri_rdf_Property $_459) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_rdf_List = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_rdf_List) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_rdf_List $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_rdf_List) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_rdf_List = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_rdf_List) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_rdf_List) true = true
% 0.99/1.20  |- ifeq (icext uri_rdf_List $X) true (icext uri_rdf_List $X) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_owl_Restriction = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_owl_Restriction) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_owl_Restriction $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_owl_Restriction) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_owl_Restriction uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_owl_Restriction = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_owl_Restriction = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_Restriction) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_Restriction) true = true
% 0.99/1.20  |- ifeq (icext uri_owl_Restriction $X) true (icext uri_owl_Restriction $X)
% 0.99/1.20       true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Restriction) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_owl_Restriction $E) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_owl_Class = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_owl_Class) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_owl_Class $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_owl_Class) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_owl_Class uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_owl_Class = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Class = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_Class uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_Class) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_Class) true = true
% 0.99/1.20  |- ifeq (icext uri_owl_Class $X) true (icext uri_owl_Class $X) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Class) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_owl_Class $E) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_ex_JoesGang = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_ex_JoesGang) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_ex_JoesGang $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_ex_JoesGang) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_ex_JoesGang uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_ex_JoesGang = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_ex_JoesGang uri_ex_JoesGang = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_ex_JoesGang uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_ex_JoesGang) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_ex_JoesGang) true = true
% 0.99/1.20  |- ifeq (icext uri_ex_JoesGang $X) true (icext uri_ex_JoesGang $X) true =
% 0.99/1.20     true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_ex_JoesGang) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_ex_JoesGang $E) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_owl_ObjectProperty = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_owl_ObjectProperty) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_owl_ObjectProperty $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_owl_ObjectProperty) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_owl_ObjectProperty uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_owl_ObjectProperty = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_owl_ObjectProperty =
% 0.99/1.20     true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_ObjectProperty) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_owl_ObjectProperty) true = true
% 0.99/1.20  |- ifeq (icext uri_owl_ObjectProperty $X) true
% 0.99/1.20       (icext uri_owl_ObjectProperty $X) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_ObjectProperty) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_owl_ObjectProperty $E) true = true
% 0.99/1.20  |- icext uri_rdfs_Class uri_rdfs_Statement = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true
% 0.99/1.20       (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true
% 0.99/1.20       (icext $D uri_rdfs_Statement) true = true
% 0.99/1.20  |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true
% 0.99/1.20  |- ic uri_rdfs_Statement = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true
% 0.99/1.20  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_rdfs_Statement) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true
% 0.99/1.20       (icext $C uri_rdfs_Statement) true = true
% 0.99/1.20  |- ifeq (icext uri_rdfs_Statement $X) true (icext uri_rdfs_Statement $X)
% 0.99/1.20       true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true
% 0.99/1.20       (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true
% 0.99/1.20       (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_owl_inverseOf) true
% 0.99/1.20       (ifeq
% 0.99/1.20          (iext $_597 sK3_testcase_premise_fullish_013_Cliques_BNODE_i
% 0.99/1.20             uri_rdf_type) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_owl_onProperty) true
% 0.99/1.20       (ifeq
% 0.99/1.20          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.20             uri_ex_sameCliqueAs) true true true) true = true
% 0.99/1.20  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_owl_propertyChainAxiom) true
% 0.99/1.20       (ifeq
% 0.99/1.20          (iext $_597 uri_foaf_knows
% 0.99/1.20             sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true true
% 0.99/1.20          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_owl_someValuesFrom) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.21             uri_ex_Clique) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_first) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.21             uri_rdf_type) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_first) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.21             uri_ex_sameCliqueAs) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_first) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.21             sK3_testcase_premise_fullish_013_Cliques_BNODE_i) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_rest) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.21             sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_rest) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.21             sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_rest) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.21             uri_rdf_nil) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.21             uri_rdf_List) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.21             uri_rdf_List) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.21             uri_rdf_List) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.21             uri_owl_Restriction) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.21             uri_rdfs_Class) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_Clique uri_owl_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_Clique uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 uri_ex_JoesGang
% 0.99/1.21             sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_JoesGang uri_ex_Clique) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_JoesGang uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_alice uri_ex_JoesGang) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_bob uri_ex_JoesGang) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_sameCliqueAs uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_foaf_knows uri_owl_ObjectProperty) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Class uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_ObjectProperty uri_rdfs_Class) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Restriction uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_inverseOf uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_onProperty uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_propertyChainAxiom uri_rdf_Property) true
% 0.99/1.21          true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_sameAs uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_someValuesFrom uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Alt uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Bag uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_List uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Property uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_XMLLiteral uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__1 uri_rdf_Property) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__1 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__2 uri_rdf_Property) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__2 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__3 uri_rdf_Property) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__3 uri_rdfs_ContainerMembershipProperty)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_first uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_nil uri_rdf_List) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_object uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_predicate uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_rest uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_subject uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_type uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_value uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Container uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Literal uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Resource uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Seq uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Statement uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_comment uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_isDefinedBy uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_label uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_member uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_range uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_seeAlso uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subClassOf uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdf_type) true
% 0.99/1.21       (ifeq (iext $_597 $_599 uri_rdfs_Resource) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_first uri_rdf_List) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_object uri_rdfs_Statement) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_predicate uri_rdfs_Statement) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_subject uri_rdfs_Statement) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_type uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_comment uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_domain uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_label uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_range uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_domain) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_sameCliqueAs uri_ex_Clique) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__1 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__2 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf__3 uri_rdfs_Resource) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_first uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_predicate uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_rest uri_rdf_List) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_subject uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_type uri_rdfs_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_value uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_comment uri_rdfs_Literal) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_domain uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_label uri_rdfs_Literal) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_member uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_range uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_seeAlso uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subClassOf uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_range) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_subPropertyOf uri_rdf_Property) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.21             sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.21             uri_rdfs_Resource) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 uri_ex_Clique
% 0.99/1.21             sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_Clique uri_ex_Clique) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_Clique uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_JoesGang uri_ex_JoesGang) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_ex_JoesGang uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Class uri_owl_Class) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Class uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_ObjectProperty uri_owl_ObjectProperty) true
% 0.99/1.21          true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_ObjectProperty uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Restriction uri_owl_Restriction) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_owl_Restriction uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Alt uri_rdf_Alt) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Alt uri_rdfs_Container) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Alt uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Bag uri_rdf_Bag) true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Bag uri_rdfs_Container) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Bag uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_List uri_rdf_List) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_List uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Property uri_rdf_Property) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_Property uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdf_XMLLiteral uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Class uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Class uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Container uri_rdfs_Container) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Container uri_rdfs_Resource) true true
% 0.99/1.21          true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 uri_rdfs_ContainerMembershipProperty
% 0.99/1.21             uri_rdfs_ContainerMembershipProperty) true true true) true =
% 0.99/1.21     true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq
% 0.99/1.21          (iext $_597 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 0.99/1.21          true true true) true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Datatype uri_rdfs_Class) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Datatype uri_rdfs_Datatype) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Datatype uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Literal uri_rdfs_Literal) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Literal uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Resource uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Seq uri_rdfs_Container) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Seq uri_rdfs_Resource) true true true)
% 0.99/1.21       true = true
% 0.99/1.21  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.21       (ifeq (iext $_597 uri_rdfs_Seq uri_rdfs_Seq) true true true) true =
% 0.99/1.21     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_Statement uri_rdfs_Resource) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subClassOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_Statement uri_rdfs_Statement) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_ex_sameCliqueAs uri_ex_sameCliqueAs) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_ex_sameCliqueAs uri_owl_sameAs) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_owl_inverseOf uri_owl_inverseOf) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_owl_onProperty uri_owl_onProperty) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq
% 0.99/1.22          (iext $_597 uri_owl_propertyChainAxiom uri_owl_propertyChainAxiom)
% 0.99/1.22          true true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_owl_sameAs uri_owl_sameAs) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_owl_someValuesFrom uri_owl_someValuesFrom) true
% 0.99/1.22          true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__1 uri_rdf__1) true true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__1 uri_rdfs_member) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__2 uri_rdf__2) true true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__2 uri_rdfs_member) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__3 uri_rdf__3) true true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf__3 uri_rdfs_member) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_first uri_rdf_first) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_object uri_rdf_object) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_predicate uri_rdf_predicate) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_rest uri_rdf_rest) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_subject uri_rdf_subject) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_type uri_rdf_type) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdf_value uri_rdf_value) true true true) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_comment uri_rdfs_comment) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_domain uri_rdfs_domain) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_label uri_rdfs_label) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_member uri_rdfs_member) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_range uri_rdfs_range) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true
% 0.99/1.22          true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf $_597 uri_rdfs_subPropertyOf) true
% 0.99/1.22       (ifeq (iext $_597 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true
% 0.99/1.22          true true) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_inverseOf $_598) true
% 0.99/1.22       (iext $_598 sK3_testcase_premise_fullish_013_Cliques_BNODE_i
% 0.99/1.22          uri_rdf_type) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_onProperty $_598) true
% 0.99/1.22       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.22          uri_ex_sameCliqueAs) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_propertyChainAxiom $_598) true
% 0.99/1.22       (iext $_598 uri_foaf_knows
% 0.99/1.22          sK1_testcase_premise_fullish_013_Cliques_BNODE_l1) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_someValuesFrom $_598) true
% 0.99/1.22       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.22          uri_ex_Clique) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_598) true
% 0.99/1.22       (iext $_598 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.22          uri_rdf_type) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_598) true
% 0.99/1.22       (iext $_598 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.22          uri_ex_sameCliqueAs) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_598) true
% 0.99/1.22       (iext $_598 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.22          sK3_testcase_premise_fullish_013_Cliques_BNODE_i) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_598) true
% 0.99/1.22       (iext $_598 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.22          sK2_testcase_premise_fullish_013_Cliques_BNODE_l2) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_598) true
% 0.99/1.22       (iext $_598 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.22          sK4_testcase_premise_fullish_013_Cliques_BNODE_l3) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_598) true
% 0.99/1.22       (iext $_598 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.22          uri_rdf_nil) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 sK1_testcase_premise_fullish_013_Cliques_BNODE_l1
% 0.99/1.22          uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 sK2_testcase_premise_fullish_013_Cliques_BNODE_l2
% 0.99/1.22          uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 sK4_testcase_premise_fullish_013_Cliques_BNODE_l3
% 0.99/1.22          uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.22          uri_owl_Restriction) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.22          uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_Clique uri_owl_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_Clique uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_JoesGang
% 0.99/1.22          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_JoesGang uri_ex_Clique) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_JoesGang uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_alice uri_ex_JoesGang) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_bob uri_ex_JoesGang) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_ex_sameCliqueAs uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_foaf_knows uri_owl_ObjectProperty) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_Class uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_ObjectProperty uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_Restriction uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_inverseOf uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_onProperty uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_propertyChainAxiom uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_sameAs uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_owl_someValuesFrom uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_Alt uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_Bag uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_List uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_Property uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_XMLLiteral uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__1 uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__2 uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__3 uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true =
% 0.99/1.22     true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_first uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_nil uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_object uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_predicate uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_rest uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_subject uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_type uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_value uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Class uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Container uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class)
% 0.99/1.22       true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Literal uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Resource uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Seq uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_Statement uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_comment uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_domain uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_isDefinedBy uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_label uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_member uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_range uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_seeAlso uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_subClassOf uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_598) true
% 0.99/1.22       (iext $_598 $_599 uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_first uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_object uri_rdfs_Statement) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_predicate uri_rdfs_Statement) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_rest uri_rdf_List) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_subject uri_rdfs_Statement) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_type uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdf_value uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_comment uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_domain uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_label uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_range uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_598) true
% 0.99/1.22       (iext $_598 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.22       (iext $_598 uri_ex_sameCliqueAs uri_ex_Clique) true = true
% 0.99/1.22  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.22       (iext $_598 uri_rdf__1 uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf__2 uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf__3 uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_first uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_predicate uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_rest uri_rdf_List) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_subject uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_type uri_rdfs_Class) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_value uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_comment uri_rdfs_Literal) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_domain uri_rdfs_Class) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_label uri_rdfs_Literal) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_member uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_range uri_rdfs_Class) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_seeAlso uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_subClassOf uri_rdfs_Class) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_598) true
% 0.99/1.23       (iext $_598 uri_rdfs_subPropertyOf uri_rdf_Property) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.23          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 sK5_testcase_premise_fullish_013_Cliques_BNODE_r
% 0.99/1.23          uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_ex_Clique
% 0.99/1.23          sK5_testcase_premise_fullish_013_Cliques_BNODE_r) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_ex_Clique uri_ex_Clique) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_ex_Clique uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_ex_JoesGang uri_ex_JoesGang) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_ex_JoesGang uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_Class uri_owl_Class) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_Class uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_ObjectProperty uri_owl_ObjectProperty) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_ObjectProperty uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_Restriction uri_owl_Restriction) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_owl_Restriction uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Alt uri_rdf_Alt) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Alt uri_rdfs_Container) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Alt uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Bag uri_rdf_Bag) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Bag uri_rdfs_Container) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_Bag uri_rdfs_Resource) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_List uri_rdf_List) true = true
% 0.99/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 0.99/1.23       (iext $_598 uri_rdf_List uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_Property uri_rdf_Property) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_Property uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Class uri_rdfs_Class) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Class uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Container uri_rdfs_Container) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Container uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_ContainerMembershipProperty uri_rdf_Property)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_ContainerMembershipProperty
% 1.08/1.23          uri_rdfs_ContainerMembershipProperty) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Datatype uri_rdfs_Class) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Datatype uri_rdfs_Datatype) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Datatype uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Literal uri_rdfs_Literal) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Literal uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Resource uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Seq uri_rdfs_Container) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Seq uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Seq uri_rdfs_Seq) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Statement uri_rdfs_Resource) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_Statement uri_rdfs_Statement) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_ex_sameCliqueAs uri_ex_sameCliqueAs) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_ex_sameCliqueAs uri_owl_sameAs) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_owl_inverseOf uri_owl_inverseOf) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_owl_onProperty uri_owl_onProperty) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_owl_propertyChainAxiom uri_owl_propertyChainAxiom)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_owl_sameAs uri_owl_sameAs) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_owl_someValuesFrom uri_owl_someValuesFrom) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__1 uri_rdf__1) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__1 uri_rdfs_member) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__2 uri_rdf__2) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__2 uri_rdfs_member) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__3 uri_rdf__3) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf__3 uri_rdfs_member) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_first uri_rdf_first) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_object uri_rdf_object) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_predicate uri_rdf_predicate) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_rest uri_rdf_rest) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_subject uri_rdf_subject) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_type uri_rdf_type) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdf_value uri_rdf_value) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_comment uri_rdfs_comment) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_domain uri_rdfs_domain) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_label uri_rdfs_label) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_member uri_rdfs_member) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_range uri_rdfs_range) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_598) true
% 1.08/1.23       (iext $_598 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true
% 1.08/1.23  |- ifeq (iext uri_ex_sameCliqueAs $_599 $_600) true
% 1.08/1.23       (iext uri_ex_sameCliqueAs $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_ex_sameCliqueAs $_599 $_600) true
% 1.08/1.23       (iext uri_owl_sameAs $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_owl_inverseOf $_599 $_600) true
% 1.08/1.23       (iext uri_owl_inverseOf $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_owl_onProperty $_599 $_600) true
% 1.08/1.23       (iext uri_owl_onProperty $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_owl_propertyChainAxiom $_599 $_600) true
% 1.08/1.23       (iext uri_owl_propertyChainAxiom $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_owl_sameAs $_599 $_600) true
% 1.08/1.23       (iext uri_owl_sameAs $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_owl_someValuesFrom $_599 $_600) true
% 1.08/1.23       (iext uri_owl_someValuesFrom $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__1 $_599 $_600) true (iext uri_rdf__1 $_599 $_600)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__1 $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_member $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__2 $_599 $_600) true (iext uri_rdf__2 $_599 $_600)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__2 $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_member $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__3 $_599 $_600) true (iext uri_rdf__3 $_599 $_600)
% 1.08/1.23       true = true
% 1.08/1.23  |- ifeq (iext uri_rdf__3 $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_member $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_first $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_first $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_object $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_object $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_predicate $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_predicate $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_rest $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_rest $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_subject $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_subject $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_type $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_type $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdf_value $_599 $_600) true
% 1.08/1.23       (iext uri_rdf_value $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_comment $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_comment $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_domain $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_domain $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_isDefinedBy $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_isDefinedBy $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_isDefinedBy $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_seeAlso $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_label $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_label $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_member $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_member $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_range $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_range $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_seeAlso $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_seeAlso $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subClassOf $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_subClassOf $_599 $_600) true = true
% 1.08/1.23  |- ifeq (iext uri_rdfs_subPropertyOf $_599 $_600) true
% 1.08/1.23       (iext uri_rdfs_subPropertyOf $_599 $_600) true = true
% 1.08/1.23  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.08/1.23  
%------------------------------------------------------------------------------