↑ Up

Metis---2.4.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SWB013+4 : TPTP v8.1.0. Released v5.2.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:21 EDT 2022

% Result   : CounterSatisfiable 0.20s 0.46s
% Output   : Saturation 0.20s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SWB013+4 : TPTP v8.1.0. Released v5.2.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n020.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 600
% 0.13/0.34  % DateTime : Wed Jun  1 01:26:38 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.20/0.46  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46  
% 0.20/0.46  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46  |- ~iext $P $S $O \/ ip $P
% 0.20/0.46  |- ir $X
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_first uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_nil uri_rdf_List
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_object uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_value uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property
% 0.20/0.46  |- ~iext uri_rdf_type $P uri_rdf_Property \/ ip $P
% 0.20/0.46  |- ~ip $P \/ iext uri_rdf_type $P uri_rdf_Property
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_type uri_rdf_Property
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource
% 0.20/0.46  |- ~icext $C $X \/ iext uri_rdf_type $X $C
% 0.20/0.46  |- ~iext uri_rdf_type $X $C \/ icext $C $X
% 0.20/0.46  |- ~ic $C \/ iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container
% 0.20/0.46  |- ~icext uri_rdfs_ContainerMembershipProperty $P \/
% 0.20/0.46     iext uri_rdfs_subPropertyOf $P uri_rdfs_member
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.20/0.46       uri_rdf_Property
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty
% 0.20/0.46  |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype
% 0.20/0.46  |- ~icext uri_rdfs_Datatype $D \/
% 0.20/0.46     iext uri_rdfs_subClassOf $D uri_rdfs_Literal
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property
% 0.20/0.46  |- ~iext $P $X $Y \/ ~iext uri_rdfs_domain $P $C \/ icext $C $X
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class
% 0.20/0.46  |- ~ic $X \/ icext uri_rdfs_Class $X
% 0.20/0.46  |- ~icext uri_rdfs_Class $X \/ ic $X
% 0.20/0.46  |- icext uri_rdfs_Resource $X
% 0.20/0.46  |- ~icext uri_rdfs_Literal $X \/ lv $X
% 0.20/0.46  |- ~lv $X \/ icext uri_rdfs_Literal $X
% 0.20/0.46  |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property
% 0.20/0.46  |- ~iext $P $X $Y \/ ~iext uri_rdfs_range $P $C \/ icext $C $Y
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class
% 0.20/0.46  |- ~iext uri_rdfs_subClassOf $C $D \/ ic $C
% 0.20/0.46  |- ~iext uri_rdfs_subClassOf $C $D \/ ic $D
% 0.20/0.46  |- ~icext $C $X \/ ~iext uri_rdfs_subClassOf $C $D \/ icext $D $X
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class
% 0.20/0.46  |- ~ic $C \/ iext uri_rdfs_subClassOf $C $C
% 0.20/0.46  |- ~iext uri_rdfs_subClassOf $C $D \/ ~iext uri_rdfs_subClassOf $D $E \/
% 0.20/0.46     iext uri_rdfs_subClassOf $C $E
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property
% 0.20/0.46  |- ~iext uri_rdfs_subPropertyOf $P $Q \/ ip $P
% 0.20/0.46  |- ~iext uri_rdfs_subPropertyOf $P $Q \/ ip $Q
% 0.20/0.46  |- ~iext $P $X $Y \/ ~iext uri_rdfs_subPropertyOf $P $Q \/ iext $Q $X $Y
% 0.20/0.46  |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property
% 0.20/0.46  |- ~ip $P \/ iext uri_rdfs_subPropertyOf $P $P
% 0.20/0.46  |- ~iext uri_rdfs_subPropertyOf $P $Q \/
% 0.20/0.46     ~iext uri_rdfs_subPropertyOf $Q $R \/ iext uri_rdfs_subPropertyOf $P $R
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class
% 0.20/0.46  |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource
% 0.20/0.46  |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource
% 0.20/0.46  |- iext uri_owl_inverseOf skolemFOFtoCNF_BNODE_i uri_rdf_type
% 0.20/0.46  |- iext uri_owl_onProperty skolemFOFtoCNF_BNODE_r uri_ex_sameCliqueAs
% 0.20/0.46  |- iext uri_owl_propertyChainAxiom uri_foaf_knows skolemFOFtoCNF_BNODE_l1
% 0.20/0.46  |- iext uri_owl_someValuesFrom skolemFOFtoCNF_BNODE_r uri_ex_Clique
% 0.20/0.46  |- iext uri_rdf_first skolemFOFtoCNF_BNODE_l1 uri_rdf_type
% 0.20/0.46  |- iext uri_rdf_first skolemFOFtoCNF_BNODE_l2 uri_ex_sameCliqueAs
% 0.20/0.46  |- iext uri_rdf_first skolemFOFtoCNF_BNODE_l3 skolemFOFtoCNF_BNODE_i
% 0.20/0.46  |- iext uri_rdf_rest skolemFOFtoCNF_BNODE_l1 skolemFOFtoCNF_BNODE_l2
% 0.20/0.46  |- iext uri_rdf_rest skolemFOFtoCNF_BNODE_l2 skolemFOFtoCNF_BNODE_l3
% 0.20/0.46  |- iext uri_rdf_rest skolemFOFtoCNF_BNODE_l3 uri_rdf_nil
% 0.20/0.46  |- iext uri_rdf_type skolemFOFtoCNF_BNODE_r uri_owl_Restriction
% 0.20/0.46  |- iext uri_rdf_type uri_ex_Clique uri_owl_Class
% 0.20/0.46  |- iext uri_rdf_type uri_ex_JoesGang uri_ex_Clique
% 0.20/0.46  |- iext uri_rdf_type uri_ex_alice uri_ex_JoesGang
% 0.20/0.46  |- iext uri_rdf_type uri_ex_bob uri_ex_JoesGang
% 0.20/0.46  |- iext uri_rdf_type uri_foaf_knows uri_owl_ObjectProperty
% 0.20/0.46  |- iext uri_rdfs_range uri_ex_sameCliqueAs uri_ex_Clique
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_ex_Clique skolemFOFtoCNF_BNODE_r
% 0.20/0.46  |- iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_owl_sameAs
% 0.20/0.46  |- ~iext uri_rdfs_domain uri_rdfs_domain $C \/ icext $C uri_rdfs_domain
% 0.20/0.46  |- ~iext uri_rdfs_range uri_rdfs_range $C \/ icext $C $C
% 0.20/0.46  |- ~iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $Q \/
% 0.20/0.46     iext $Q uri_rdfs_subPropertyOf $Q
% 0.20/0.46  |- ~iext uri_foaf_knows uri_ex_alice uri_ex_bob
% 0.20/0.46  |- icext uri_rdf_Property uri_rdfs_domain
% 0.20/0.46  |- icext uri_rdfs_Class uri_rdfs_Class
% 0.20/0.46  |- ic uri_rdfs_Class
% 0.20/0.46  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource
% 0.20/0.47  |- ip uri_rdf__1
% 0.20/0.47  |- ip uri_rdf__2
% 0.20/0.47  |- ip uri_rdf__3
% 0.20/0.47  |- ip uri_rdf_first
% 0.20/0.47  |- ip uri_rdf_object
% 0.20/0.47  |- ip uri_rdf_rest
% 0.20/0.47  |- ip uri_rdf_subject
% 0.20/0.47  |- ip uri_rdf_type
% 0.20/0.47  |- ip uri_rdf_value
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value
% 0.20/0.47  |- ic skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- ic uri_rdfs_Container
% 0.20/0.47  |- ic uri_rdfs_Literal
% 0.20/0.47  |- ic uri_rdfs_Resource
% 0.20/0.47  |- ic uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subClassOf skolemFOFtoCNF_BNODE_r skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- iext uri_rdfs_subClassOf skolemFOFtoCNF_BNODE_r uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_Container
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_Literal
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_Resource
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdf_Property
% 0.20/0.47  |- ic uri_ex_Clique
% 0.20/0.47  |- ic uri_rdf_Alt
% 0.20/0.47  |- ic uri_rdf_Bag
% 0.20/0.47  |- ic uri_rdf_XMLLiteral
% 0.20/0.47  |- ic uri_rdfs_ContainerMembershipProperty
% 0.20/0.47  |- ic uri_rdfs_Datatype
% 0.20/0.47  |- ic uri_rdfs_Seq
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdf_XMLLiteral
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.20/0.47       uri_rdfs_ContainerMembershipProperty
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty
% 0.20/0.47       uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_Seq
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_ex_Clique uri_ex_Clique
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_ex_Clique uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_ex_Clique
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdf_Alt
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdf_Bag
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype
% 0.20/0.47  |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource
% 0.20/0.47  |- icext uri_rdfs_Class uri_rdfs_Datatype
% 0.20/0.47  |- ip uri_ex_sameCliqueAs
% 0.20/0.47  |- ip uri_rdfs_isDefinedBy
% 0.20/0.47  |- iext uri_rdf_type uri_ex_sameCliqueAs uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_ex_sameCliqueAs uri_ex_sameCliqueAs
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy
% 0.20/0.47  |- ip uri_owl_sameAs
% 0.20/0.47  |- ip uri_rdfs_seeAlso
% 0.20/0.47  |- iext uri_rdf_type uri_owl_sameAs uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_owl_sameAs uri_owl_sameAs
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property
% 0.20/0.47  |- iext uri_rdf_type skolemFOFtoCNF_BNODE_r uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_ex_Clique uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class
% 0.20/0.47  |- iext uri_rdf_type $_25 uri_rdfs_Resource
% 0.20/0.47  |- ip uri_rdfs_domain
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain
% 0.20/0.47  |- icext uri_owl_Restriction skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- icext uri_owl_Class uri_ex_Clique
% 0.20/0.47  |- icext uri_ex_Clique uri_ex_JoesGang
% 0.20/0.47  |- icext uri_ex_JoesGang uri_ex_alice
% 0.20/0.47  |- icext uri_ex_JoesGang uri_ex_bob
% 0.20/0.47  |- icext uri_rdf_Property uri_ex_sameCliqueAs
% 0.20/0.47  |- icext uri_owl_ObjectProperty uri_foaf_knows
% 0.20/0.47  |- icext uri_rdf_Property uri_owl_sameAs
% 0.20/0.47  |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf__1
% 0.20/0.47  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf__2
% 0.20/0.47  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf__3
% 0.20/0.47  |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_first
% 0.20/0.47  |- icext uri_rdf_List uri_rdf_nil
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_object
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_rest
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_subject
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_type
% 0.20/0.47  |- icext uri_rdf_Property uri_rdf_value
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_isDefinedBy
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_seeAlso
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member
% 0.20/0.47  |- ip uri_rdfs_member
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_member
% 0.20/0.47  |- ip uri_owl_inverseOf
% 0.20/0.47  |- ip uri_owl_onProperty
% 0.20/0.47  |- ip uri_owl_propertyChainAxiom
% 0.20/0.47  |- ip uri_owl_someValuesFrom
% 0.20/0.47  |- ip uri_rdfs_range
% 0.20/0.47  |- ip uri_rdfs_subClassOf
% 0.20/0.47  |- ip uri_rdfs_subPropertyOf
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf
% 0.20/0.47  |- iext uri_rdf_type uri_owl_inverseOf uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_owl_inverseOf uri_owl_inverseOf
% 0.20/0.47  |- iext uri_rdf_type uri_owl_onProperty uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_owl_onProperty uri_owl_onProperty
% 0.20/0.47  |- iext uri_rdf_type uri_owl_propertyChainAxiom uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_owl_propertyChainAxiom
% 0.20/0.47       uri_owl_propertyChainAxiom
% 0.20/0.47  |- iext uri_rdf_type uri_owl_someValuesFrom uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_owl_someValuesFrom
% 0.20/0.47       uri_owl_someValuesFrom
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range
% 0.20/0.47  |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property
% 0.20/0.47  |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.20/0.47       uri_rdfs_subPropertyOf
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_subClassOf
% 0.20/0.47  |- icext uri_rdf_Property uri_owl_inverseOf
% 0.20/0.47  |- icext uri_rdf_Property uri_owl_onProperty
% 0.20/0.47  |- icext uri_rdf_Property uri_owl_propertyChainAxiom
% 0.20/0.47  |- icext uri_rdf_Property uri_owl_someValuesFrom
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_range
% 0.20/0.47  |- icext uri_rdf_Property uri_rdfs_subPropertyOf
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf uri_rdfs_Resource $_33 \/ icext $_33 $_34
% 0.20/0.47  |- ~icext uri_ex_Clique $_34 \/ icext skolemFOFtoCNF_BNODE_r $_34
% 0.20/0.47  |- ~icext uri_rdf_Alt $_34 \/ icext uri_rdfs_Container $_34
% 0.20/0.47  |- ~icext uri_rdf_Bag $_34 \/ icext uri_rdfs_Container $_34
% 0.20/0.47  |- ~icext uri_rdf_XMLLiteral $_34 \/ icext uri_rdfs_Literal $_34
% 0.20/0.47  |- ~icext uri_rdfs_ContainerMembershipProperty $_34 \/
% 0.20/0.47     icext uri_rdf_Property $_34
% 0.20/0.47  |- ~icext uri_rdfs_Datatype $_34 \/ icext uri_rdfs_Class $_34
% 0.20/0.47  |- ~icext uri_rdfs_Seq $_34 \/ icext uri_rdfs_Container $_34
% 0.20/0.47  |- icext skolemFOFtoCNF_BNODE_r uri_ex_JoesGang
% 0.20/0.47  |- iext uri_rdf_type uri_ex_JoesGang skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf skolemFOFtoCNF_BNODE_r $_46 \/
% 0.20/0.47     iext uri_rdfs_subClassOf uri_ex_Clique $_46
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf uri_rdf_Property $_46 \/
% 0.20/0.47     iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_46
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf uri_rdfs_Class $_46 \/
% 0.20/0.47     iext uri_rdfs_subClassOf uri_rdfs_Datatype $_46
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf uri_rdfs_Container $_46 \/
% 0.20/0.47     iext uri_rdfs_subClassOf uri_rdfs_Seq $_46
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf uri_rdfs_Resource $_46 \/
% 0.20/0.47     iext uri_rdfs_subClassOf uri_rdfs_Seq $_46
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 skolemFOFtoCNF_BNODE_r \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_ex_Clique \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 skolemFOFtoCNF_BNODE_r
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_ex_Clique \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_Alt \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Container
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_Alt \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_Bag \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Container
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_Bag \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_Property \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_XMLLiteral \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Literal
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdf_XMLLiteral \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Class \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Container \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_ContainerMembershipProperty \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdf_Property
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_ContainerMembershipProperty \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Datatype \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Class
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Datatype \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Literal \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Seq \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Container
% 0.20/0.47  |- ~iext uri_rdfs_subClassOf $_44 uri_rdfs_Seq \/
% 0.20/0.47     iext uri_rdfs_subClassOf $_44 uri_rdfs_Resource
% 0.20/0.47  |- ~iext uri_rdfs_subPropertyOf $_71 uri_ex_sameCliqueAs \/
% 0.20/0.47     iext uri_rdfs_subPropertyOf $_71 uri_owl_sameAs
% 0.20/0.47  |- ~iext uri_rdfs_subPropertyOf $_71 uri_rdf__1 \/
% 0.20/0.47     iext uri_rdfs_subPropertyOf $_71 uri_rdfs_member
% 0.20/0.47  |- ~iext uri_rdfs_subPropertyOf $_71 uri_rdf__2 \/
% 0.20/0.47     iext uri_rdfs_subPropertyOf $_71 uri_rdfs_member
% 0.20/0.47  |- ~iext uri_rdfs_subPropertyOf $_71 uri_rdf__3 \/
% 0.20/0.47     iext uri_rdfs_subPropertyOf $_71 uri_rdfs_member
% 0.20/0.47  |- ~iext uri_rdfs_subPropertyOf $_71 uri_rdfs_isDefinedBy \/
% 0.20/0.47     iext uri_rdfs_subPropertyOf $_71 uri_rdfs_seeAlso
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdf_type $_79 \/ icext $_79 $_81
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/
% 0.20/0.47     icext $_79 uri_rdfs_isDefinedBy
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/ icext $_79 uri_rdfs_label
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/ icext $_79 uri_rdfs_member
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/ icext $_79 uri_rdfs_range
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/
% 0.20/0.47     icext $_79 uri_rdfs_seeAlso
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/
% 0.20/0.47     icext $_79 uri_rdfs_subClassOf
% 0.20/0.47  |- ~iext uri_rdfs_domain uri_rdfs_domain $_79 \/
% 0.20/0.47     icext $_79 uri_rdfs_subPropertyOf
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/
% 0.20/0.48     icext $_79 uri_ex_sameCliqueAs
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf__1
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf__2
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf__3
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf_first
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_predicate
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf_rest
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf_subject
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf_type
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdf_value
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_comment
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_domain
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_isDefinedBy
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_label
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_member
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_range
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/ icext $_79 uri_rdfs_seeAlso
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_subClassOf
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_range $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_subPropertyOf
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 skolemFOFtoCNF_BNODE_r
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_ex_Clique
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/ icext $_79 uri_rdf_Alt
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/ icext $_79 uri_rdf_Bag
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_Property
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_XMLLiteral
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Class
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Container
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_ContainerMembershipProperty
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Datatype
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Literal
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_Seq
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_ex_sameCliqueAs
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_owl_inverseOf
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_owl_onProperty
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_owl_propertyChainAxiom
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_owl_sameAs
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_owl_someValuesFrom
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf__1
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf__2
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf__3
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_first
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_object
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_rest
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_subject
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_type
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdf_value
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_domain
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_isDefinedBy
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_member
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_range
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_seeAlso
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_subClassOf
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $_79 \/
% 0.20/0.48     icext $_79 uri_rdfs_subPropertyOf
% 0.20/0.48  |- ~iext uri_rdf_first $_81 $_82 \/ icext uri_rdf_List $_81
% 0.20/0.48  |- ~iext uri_rdf_object $_81 $_82 \/ icext uri_rdfs_Statement $_81
% 0.20/0.48  |- ~iext uri_rdf_predicate $_81 $_82 \/ icext uri_rdfs_Statement $_81
% 0.20/0.48  |- ~iext uri_rdf_rest $_81 $_82 \/ icext uri_rdf_List $_81
% 0.20/0.48  |- ~iext uri_rdf_subject $_81 $_82 \/ icext uri_rdfs_Statement $_81
% 0.20/0.48  |- ~iext uri_rdfs_domain $_81 $_82 \/ icext uri_rdf_Property $_81
% 0.20/0.48  |- icext uri_rdf_Property uri_rdfs_label
% 0.20/0.48  |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property
% 0.20/0.48  |- ip uri_rdfs_label
% 0.20/0.48  |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $C \/
% 0.20/0.48     icext $C uri_rdfs_label
% 0.20/0.48  |- icext uri_rdf_Property uri_rdf_predicate
% 0.20/0.48  |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property
% 0.20/0.48  |- ip uri_rdf_predicate
% 0.20/0.48  |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $C \/
% 0.20/0.48     icext $C uri_rdf_predicate
% 0.20/0.48  |- icext uri_rdf_Property uri_rdfs_comment
% 0.20/0.48  |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property
% 0.20/0.48  |- ip uri_rdfs_comment
% 0.20/0.48  |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subPropertyOf $C \/
% 0.20/0.48     icext $C uri_rdfs_comment
% 0.20/0.48  |- icext uri_rdf_List skolemFOFtoCNF_BNODE_l1
% 0.20/0.48  |- icext uri_rdf_List skolemFOFtoCNF_BNODE_l2
% 0.20/0.48  |- icext uri_rdf_List skolemFOFtoCNF_BNODE_l3
% 0.20/0.48  |- iext uri_rdf_type skolemFOFtoCNF_BNODE_l1 uri_rdf_List
% 0.20/0.48  |- iext uri_rdf_type skolemFOFtoCNF_BNODE_l2 uri_rdf_List
% 0.20/0.48  |- iext uri_rdf_type skolemFOFtoCNF_BNODE_l3 uri_rdf_List
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdf_type $_161 \/ icext $_161 uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_range $_161 \/ icext $_161 uri_rdfs_Class
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_range $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_range $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_Property
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 skolemFOFtoCNF_BNODE_r
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_ex_Clique
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_Alt
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Container
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_Bag
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_Property
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_XMLLiteral
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Literal
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Class
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_ContainerMembershipProperty
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Datatype
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_Seq
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_ex_sameCliqueAs
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_owl_sameAs
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_owl_inverseOf
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_owl_onProperty
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_owl_propertyChainAxiom
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_owl_someValuesFrom
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf__1
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_member
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf__2
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf__3
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_first
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_object
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_predicate
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_rest
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_subject
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_type
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdf_value
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_comment
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_domain
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_isDefinedBy
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_seeAlso
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_label
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_range
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_subClassOf
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subPropertyOf $_161 \/
% 0.20/0.48     icext $_161 uri_rdfs_subPropertyOf
% 0.20/0.48  |- ~iext uri_ex_sameCliqueAs $_163 $_164 \/ icext uri_ex_Clique $_164
% 0.20/0.48  |- ~iext uri_rdf_rest $_163 $_164 \/ icext uri_rdf_List $_164
% 0.20/0.48  |- ~iext uri_rdf_type $_163 $_164 \/ icext uri_rdfs_Class $_164
% 0.20/0.48  |- ~iext uri_rdfs_comment $_163 $_164 \/ icext uri_rdfs_Literal $_164
% 0.20/0.48  |- ~iext uri_rdfs_domain $_163 $_164 \/ icext uri_rdfs_Class $_164
% 0.20/0.48  |- ~iext uri_rdfs_label $_163 $_164 \/ icext uri_rdfs_Literal $_164
% 0.20/0.48  |- ~iext uri_rdfs_range $_163 $_164 \/ icext uri_rdfs_Class $_164
% 0.20/0.48  |- icext uri_rdfs_Class uri_rdf_List
% 0.20/0.48  |- icext uri_rdfs_Class uri_owl_Restriction
% 0.20/0.48  |- icext uri_rdfs_Class uri_owl_Class
% 0.20/0.48  |- icext uri_rdfs_Class uri_ex_JoesGang
% 0.20/0.48  |- icext uri_rdfs_Class uri_owl_ObjectProperty
% 0.20/0.48  |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class
% 0.20/0.48  |- ic uri_rdf_List
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource
% 0.20/0.48  |- iext uri_rdf_type uri_owl_Restriction uri_rdfs_Class
% 0.20/0.48  |- ic uri_owl_Restriction
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_owl_Restriction
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_rdfs_Resource
% 0.20/0.48  |- iext uri_rdf_type uri_owl_Class uri_rdfs_Class
% 0.20/0.48  |- ic uri_owl_Class
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Class
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_Class uri_rdfs_Resource
% 0.20/0.48  |- iext uri_rdf_type uri_ex_JoesGang uri_rdfs_Class
% 0.20/0.48  |- ic uri_ex_JoesGang
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_ex_JoesGang uri_ex_JoesGang
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_ex_JoesGang uri_rdfs_Resource
% 0.20/0.48  |- iext uri_rdf_type uri_owl_ObjectProperty uri_rdfs_Class
% 0.20/0.48  |- ic uri_owl_ObjectProperty
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_owl_ObjectProperty
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/ icext $C uri_rdf_List
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/ icext $C uri_rdf_List
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_rdf_List \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_owl_Restriction
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_owl_Restriction
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_owl_Restriction \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/ icext $C uri_owl_Class
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/ icext $C uri_owl_Class
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_owl_Class \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/ icext $C uri_ex_JoesGang
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/ icext $C uri_ex_JoesGang
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_ex_JoesGang \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_owl_ObjectProperty
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_owl_ObjectProperty
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_owl_ObjectProperty \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- icext uri_rdfs_Class uri_rdfs_Statement
% 0.20/0.48  |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class
% 0.20/0.48  |- ic uri_rdfs_Statement
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement
% 0.20/0.48  |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_range uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_rdfs_Statement
% 0.20/0.48  |- ~iext uri_rdfs_domain uri_rdfs_subClassOf $C \/
% 0.20/0.48     icext $C uri_rdfs_Statement
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf $C uri_rdfs_Statement \/
% 0.20/0.48     iext uri_rdfs_subClassOf $C uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_subClassOf uri_rdfs_Resource $E \/
% 0.20/0.48     iext uri_rdfs_subClassOf uri_rdfs_Statement $E
% 0.20/0.48  |- ~iext uri_rdfs_subPropertyOf uri_rdf_type $_241 \/
% 0.20/0.48     iext $_241 $_242 uri_rdfs_Resource
% 0.20/0.48  |- ~iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_241 \/
% 0.20/0.48     iext $_241 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf
% 0.20/0.48  |- ~iext uri_ex_sameCliqueAs $_242 $_243 \/ iext uri_owl_sameAs $_242 $_243
% 0.20/0.48  |- ~iext uri_rdf__1 $_242 $_243 \/ iext uri_rdfs_member $_242 $_243
% 0.20/0.48  |- ~iext uri_rdf__2 $_242 $_243 \/ iext uri_rdfs_member $_242 $_243
% 0.20/0.48  |- ~iext uri_rdf__3 $_242 $_243 \/ iext uri_rdfs_member $_242 $_243
% 0.20/0.48  |- ~iext uri_rdfs_isDefinedBy $_242 $_243 \/
% 0.20/0.48     iext uri_rdfs_seeAlso $_242 $_243
% 0.20/0.48  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.48  
%------------------------------------------------------------------------------