%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWB013+4 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n017.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 : 0s
% DateTime : Tue Jul 19 18:47:35 EDT 2022
% Result : CounterSatisfiable 0.70s 1.10s
% Output : Saturation 0.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SWB013+4 : TPTP v8.1.0. Released v5.2.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n017.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 % DateTime : Wed Jun 1 00:45:41 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.70/1.09 *** allocated 10000 integers for termspace/termends
% 0.70/1.09 *** allocated 10000 integers for clauses
% 0.70/1.09 *** allocated 10000 integers for justifications
% 0.70/1.09 Bliksem 1.12
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Automatic Strategy Selection
% 0.70/1.09
% 0.70/1.09
% 0.70/1.09 Clauses:
% 0.70/1.09
% 0.70/1.09 { ! iext( X, Y, Z ), ip( X ) }.
% 0.70/1.09 { ir( X ) }.
% 0.70/1.09 { ! lv( X ), ir( X ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_first, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_nil, uri_rdf_List ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_rest, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__1, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__2, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__3, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_object, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_value, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_subject, uri_rdf_Property ) }.
% 0.70/1.09 { ! iext( uri_rdf_type, X, uri_rdf_Property ), ip( X ) }.
% 0.70/1.09 { ! ip( X ), iext( uri_rdf_type, X, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_type, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_type, uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso ) }
% 0.70/1.09 .
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource ) }.
% 0.70/1.09 { ! iext( uri_rdf_type, X, Y ), icext( Y, X ) }.
% 0.70/1.09 { ! icext( Y, X ), iext( uri_rdf_type, X, Y ) }.
% 0.70/1.09 { ! ic( X ), iext( uri_rdfs_subClassOf, X, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdf_first, uri_rdf_List ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdf_rest, uri_rdf_List ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdf_rest, uri_rdf_List ) }.
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container ) }.
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container ) }.
% 0.70/1.09 { ! icext( uri_rdfs_ContainerMembershipProperty, X ), iext(
% 0.70/1.09 uri_rdfs_subPropertyOf, X, uri_rdfs_member ) }.
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty,
% 0.70/1.09 uri_rdf_Property ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty ) }
% 0.70/1.09 .
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty ) }
% 0.70/1.09 .
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty ) }
% 0.70/1.09 .
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container ) }.
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype ) }.
% 0.70/1.09 { ! icext( uri_rdfs_Datatype, X ), iext( uri_rdfs_subClassOf, X,
% 0.70/1.09 uri_rdfs_Literal ) }.
% 0.70/1.09 { iext( uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property ) }.
% 0.70/1.09 { ! iext( uri_rdfs_domain, Z, X ), ! iext( Z, Y, T ), icext( X, Y ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class ) }.
% 0.70/1.09 { ! ic( X ), icext( uri_rdfs_Class, X ) }.
% 0.70/1.09 { ! icext( uri_rdfs_Class, X ), ic( X ) }.
% 0.70/1.09 { ! ir( X ), icext( uri_rdfs_Resource, X ) }.
% 0.70/1.09 { ! icext( uri_rdfs_Resource, X ), ir( X ) }.
% 0.70/1.09 { ! lv( X ), icext( uri_rdfs_Literal, X ) }.
% 0.70/1.09 { ! icext( uri_rdfs_Literal, X ), lv( X ) }.
% 0.70/1.09 { iext( uri_rdf_type, uri_rdf_Property, uri_rdfs_Class ) }.
% 0.70/1.09 { iext( uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property ) }.
% 0.70/1.09 { ! iext( uri_rdfs_range, Z, X ), ! iext( Z, T, Y ), icext( X, Y ) }.
% 0.70/1.09 { iext( uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subClassOf, X, Y ), ic( X ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subClassOf, X, Y ), ic( Y ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subClassOf, X, Y ), ! icext( X, Z ), icext( Y, Z ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class ) }.
% 0.70/1.10 { ! ic( X ), iext( uri_rdfs_subClassOf, X, X ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subClassOf, X, Z ), ! iext( uri_rdfs_subClassOf, Z, Y )
% 0.70/1.10 , iext( uri_rdfs_subClassOf, X, Y ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subPropertyOf, X, Y ), ip( X ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subPropertyOf, X, Y ), ip( Y ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subPropertyOf, X, Y ), ! iext( X, Z, T ), iext( Y, Z, T
% 0.70/1.10 ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.70/1.10 { ! ip( X ), iext( uri_rdfs_subPropertyOf, X, X ) }.
% 0.70/1.10 { ! iext( uri_rdfs_subPropertyOf, X, Z ), ! iext( uri_rdfs_subPropertyOf, Z
% 0.70/1.10 , Y ), iext( uri_rdfs_subPropertyOf, X, Y ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdf_type, uri_rdfs_Class ) }.
% 0.70/1.10 { iext( uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource ) }.
% 0.70/1.10 { ! iext( uri_foaf_knows, uri_ex_alice, uri_ex_bob ) }.
% 0.70/1.10 { iext( uri_rdf_type, uri_ex_Clique, uri_owl_Class ) }.
% 0.70/1.10 { iext( uri_rdfs_subPropertyOf, uri_ex_sameCliqueAs, uri_owl_sameAs ) }.
% 0.70/1.10 { iext( uri_rdfs_range, uri_ex_sameCliqueAs, uri_ex_Clique ) }.
% 0.70/1.10 { iext( uri_rdfs_subClassOf, uri_ex_Clique, skol1 ) }.
% 0.70/1.10 { iext( uri_rdf_type, skol1, uri_owl_Restriction ) }.
% 0.70/1.10 { iext( uri_owl_onProperty, skol1, uri_ex_sameCliqueAs ) }.
% 0.70/1.10 { iext( uri_owl_someValuesFrom, skol1, uri_ex_Clique ) }.
% 0.70/1.10 { iext( uri_rdf_type, uri_foaf_knows, uri_owl_ObjectProperty ) }.
% 0.70/1.10 { iext( uri_owl_propertyChainAxiom, uri_foaf_knows, skol2 ) }.
% 0.70/1.10 { iext( uri_rdf_first, skol2, uri_rdf_type ) }.
% 0.70/1.10 { iext( uri_rdf_rest, skol2, skol3 ) }.
% 0.70/1.10 { iext( uri_rdf_first, skol3, uri_ex_sameCliqueAs ) }.
% 0.70/1.10 { iext( uri_rdf_rest, skol3, skol4 ) }.
% 0.70/1.10 { iext( uri_rdf_first, skol4, skol5 ) }.
% 0.70/1.10 { iext( uri_rdf_rest, skol4, uri_rdf_nil ) }.
% 0.70/1.10 { iext( uri_owl_inverseOf, skol5, uri_rdf_type ) }.
% 0.70/1.10 { iext( uri_rdf_type, uri_ex_JoesGang, uri_ex_Clique ) }.
% 0.70/1.10 { iext( uri_rdf_type, uri_ex_alice, uri_ex_JoesGang ) }.
% 0.70/1.10 { iext( uri_rdf_type, uri_ex_bob, uri_ex_JoesGang ) }.
% 0.70/1.10
% 0.70/1.10 percentage equality = 0.000000, percentage horn = 1.000000
% 0.70/1.10 This is a near-Horn, non-equality problem
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Options Used:
% 0.70/1.10
% 0.70/1.10 useres = 1
% 0.70/1.10 useparamod = 0
% 0.70/1.10 useeqrefl = 0
% 0.70/1.10 useeqfact = 0
% 0.70/1.10 usefactor = 1
% 0.70/1.10 usesimpsplitting = 0
% 0.70/1.10 usesimpdemod = 0
% 0.70/1.10 usesimpres = 4
% 0.70/1.10
% 0.70/1.10 resimpinuse = 1000
% 0.70/1.10 resimpclauses = 20000
% 0.70/1.10 substype = standard
% 0.70/1.10 backwardsubs = 1
% 0.70/1.10 selectoldest = 5
% 0.70/1.10
% 0.70/1.10 litorderings [0] = split
% 0.70/1.10 litorderings [1] = liftord
% 0.70/1.10
% 0.70/1.10 termordering = none
% 0.70/1.10
% 0.70/1.10 litapriori = 1
% 0.70/1.10 termapriori = 0
% 0.70/1.10 litaposteriori = 0
% 0.70/1.10 termaposteriori = 0
% 0.70/1.10 demodaposteriori = 0
% 0.70/1.10 ordereqreflfact = 0
% 0.70/1.10
% 0.70/1.10 litselect = negative
% 0.70/1.10
% 0.70/1.10 maxweight = 30000
% 0.70/1.10 maxdepth = 30000
% 0.70/1.10 maxlength = 115
% 0.70/1.10 maxnrvars = 195
% 0.70/1.10 excuselevel = 0
% 0.70/1.10 increasemaxweight = 0
% 0.70/1.10
% 0.70/1.10 maxselected = 10000000
% 0.70/1.10 maxnrclauses = 10000000
% 0.70/1.10
% 0.70/1.10 showgenerated = 0
% 0.70/1.10 showkept = 0
% 0.70/1.10 showselected = 0
% 0.70/1.10 showdeleted = 0
% 0.70/1.10 showresimp = 1
% 0.70/1.10 showstatus = 2000
% 0.70/1.10
% 0.70/1.10 prologoutput = 0
% 0.70/1.10 nrgoals = 5000000
% 0.70/1.10 totalproof = 1
% 0.70/1.10
% 0.70/1.10 Symbols occurring in the translation:
% 0.70/1.10
% 0.70/1.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.70/1.10 . [1, 2] (w:1, o:82, a:1, s:1, b:0),
% 0.70/1.10 ! [4, 1] (w:1, o:73, a:1, s:1, b:0),
% 0.70/1.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.70/1.10 iext [38, 3] (w:1, o:107, a:1, s:1, b:0),
% 0.70/1.10 ip [39, 1] (w:1, o:78, a:1, s:1, b:0),
% 0.70/1.10 ir [41, 1] (w:1, o:79, a:1, s:1, b:0),
% 0.70/1.10 lv [42, 1] (w:1, o:80, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_type [43, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_first [44, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_Property [45, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_nil [46, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_List [47, 0] (w:1, o:16, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_rest [48, 0] (w:1, o:17, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf__1 [49, 0] (w:1, o:18, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf__2 [50, 0] (w:1, o:19, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf__3 [51, 0] (w:1, o:20, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_object [52, 0] (w:1, o:21, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_value [53, 0] (w:1, o:22, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_subject [54, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_domain [55, 0] (w:1, o:24, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_comment [56, 0] (w:1, o:23, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Resource [57, 0] (w:1, o:25, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_range [58, 0] (w:1, o:26, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Literal [59, 0] (w:1, o:27, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_isDefinedBy [60, 0] (w:1, o:28, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_subPropertyOf [61, 0] (w:1, o:29, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_seeAlso [62, 0] (w:1, o:30, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_label [63, 0] (w:1, o:31, a:1, s:1, b:0),
% 0.70/1.10 icext [65, 2] (w:1, o:106, a:1, s:1, b:0),
% 0.70/1.10 ic [66, 1] (w:1, o:81, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_subClassOf [67, 0] (w:1, o:38, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_Alt [68, 0] (w:1, o:39, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Container [69, 0] (w:1, o:40, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_Bag [70, 0] (w:1, o:41, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty [71, 0] (w:1, o:42, a:1, s:1, b:
% 0.70/1.10 0),
% 0.70/1.10 uri_rdfs_member [72, 0] (w:1, o:43, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Seq [73, 0] (w:1, o:44, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_XMLLiteral [74, 0] (w:1, o:45, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Datatype [75, 0] (w:1, o:47, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Class [77, 0] (w:1, o:46, a:1, s:1, b:0),
% 0.70/1.10 uri_rdfs_Statement [79, 0] (w:1, o:50, a:1, s:1, b:0),
% 0.70/1.10 uri_rdf_predicate [80, 0] (w:1, o:51, a:1, s:1, b:0),
% 0.70/1.10 uri_foaf_knows [84, 0] (w:1, o:59, a:1, s:1, b:0),
% 0.70/1.10 uri_ex_alice [85, 0] (w:1, o:54, a:1, s:1, b:0),
% 0.70/1.10 uri_ex_bob [86, 0] (w:1, o:55, a:1, s:1, b:0),
% 0.70/1.10 uri_ex_Clique [92, 0] (w:1, o:56, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_Class [93, 0] (w:1, o:60, a:1, s:1, b:0),
% 0.70/1.10 uri_ex_sameCliqueAs [94, 0] (w:1, o:57, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_sameAs [95, 0] (w:1, o:61, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_Restriction [96, 0] (w:1, o:62, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_onProperty [97, 0] (w:1, o:63, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_someValuesFrom [98, 0] (w:1, o:64, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_ObjectProperty [99, 0] (w:1, o:65, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_propertyChainAxiom [100, 0] (w:1, o:66, a:1, s:1, b:0),
% 0.70/1.10 uri_owl_inverseOf [101, 0] (w:1, o:67, a:1, s:1, b:0),
% 0.70/1.10 uri_ex_JoesGang [102, 0] (w:1, o:58, a:1, s:1, b:0),
% 0.70/1.10 skol1 [103, 0] (w:1, o:68, a:1, s:1, b:0),
% 0.70/1.10 skol2 [104, 0] (w:1, o:69, a:1, s:1, b:0),
% 0.70/1.10 skol3 [105, 0] (w:1, o:70, a:1, s:1, b:0),
% 0.70/1.10 skol4 [106, 0] (w:1, o:71, a:1, s:1, b:0),
% 0.70/1.10 skol5 [107, 0] (w:1, o:72, a:1, s:1, b:0).
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 Starting Search:
% 0.70/1.10
% 0.70/1.10 *** allocated 15000 integers for clauses
% 0.70/1.10 *** allocated 22500 integers for clauses
% 0.70/1.10 *** allocated 33750 integers for clauses
% 0.70/1.10 *** allocated 50625 integers for clauses
% 0.70/1.10 Resimplifying inuse:
% 0.70/1.10 Done
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10
% 0.70/1.10 found a saturation!
% 0.70/1.10 % SZS status CounterSatisfiable
% 0.70/1.10 % SZS output start Saturation
% 0.70/1.10
% 0.70/1.10 (471) {G1,W9,D2,L2,V1,M1} R(77,104) { iext( X, uri_ex_bob, uri_ex_JoesGang
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (470) {G1,W9,D2,L2,V1,M1} R(77,103) { iext( X, uri_ex_alice,
% 0.70/1.10 uri_ex_JoesGang ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (469) {G1,W9,D2,L2,V1,M1} R(77,102) { iext( X, uri_ex_JoesGang,
% 0.70/1.10 uri_ex_Clique ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (468) {G1,W9,D2,L2,V1,M1} R(77,101) { iext( X, skol5, uri_rdf_type ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_owl_inverseOf, X ) }.
% 0.70/1.10 (467) {G1,W9,D2,L2,V1,M1} R(77,100) { iext( X, skol4, uri_rdf_nil ), ! iext
% 0.70/1.10 ( uri_rdfs_subPropertyOf, uri_rdf_rest, X ) }.
% 0.70/1.10 (466) {G1,W9,D2,L2,V1,M1} R(77,2) { iext( X, uri_rdf_first,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (465) {G1,W9,D2,L2,V1,M1} R(77,99) { iext( X, skol4, skol5 ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdf_first, X ) }.
% 0.70/1.10 (464) {G1,W9,D2,L2,V1,M1} R(77,98) { iext( X, skol3, skol4 ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdf_rest, X ) }.
% 0.70/1.10 (463) {G1,W9,D2,L2,V1,M1} R(77,3) { iext( X, uri_rdf_nil, uri_rdf_List ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (462) {G1,W9,D2,L2,V1,M1} R(77,97) { iext( X, skol3, uri_ex_sameCliqueAs )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdf_first, X ) }.
% 0.70/1.10 (461) {G1,W9,D2,L2,V1,M1} R(77,96) { iext( X, skol2, skol3 ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdf_rest, X ) }.
% 0.70/1.10 (460) {G1,W9,D2,L2,V1,M1} R(77,95) { iext( X, skol2, uri_rdf_type ), ! iext
% 0.70/1.10 ( uri_rdfs_subPropertyOf, uri_rdf_first, X ) }.
% 0.70/1.10 (459) {G1,W9,D2,L2,V1,M1} R(77,94) { iext( X, uri_foaf_knows, skol2 ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, X ) }.
% 0.70/1.10 (458) {G1,W9,D2,L2,V1,M1} R(77,4) { iext( X, uri_rdf_rest, uri_rdf_Property
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (457) {G1,W9,D2,L2,V1,M1} R(77,93) { iext( X, uri_foaf_knows,
% 0.70/1.10 uri_owl_ObjectProperty ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X
% 0.70/1.10 ) }.
% 0.70/1.10 (456) {G1,W9,D2,L2,V1,M1} R(77,92) { iext( X, skol1, uri_ex_Clique ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, X ) }.
% 0.70/1.10 (455) {G1,W9,D2,L2,V1,M1} R(77,5) { iext( X, uri_rdf__1, uri_rdf_Property )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (454) {G1,W9,D2,L2,V1,M1} R(77,91) { iext( X, skol1, uri_ex_sameCliqueAs )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_owl_onProperty, X ) }.
% 0.70/1.10 (453) {G1,W9,D2,L2,V1,M1} R(77,90) { iext( X, skol1, uri_owl_Restriction )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (452) {G1,W9,D2,L2,V1,M1} R(77,89) { iext( X, uri_ex_Clique, skol1 ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (451) {G1,W9,D2,L2,V1,M1} R(77,6) { iext( X, uri_rdf__2, uri_rdf_Property )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (450) {G1,W9,D2,L2,V1,M1} R(77,88) { iext( X, uri_ex_sameCliqueAs,
% 0.70/1.10 uri_ex_Clique ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (449) {G1,W9,D2,L2,V1,M1} R(77,87) { iext( X, uri_ex_sameCliqueAs,
% 0.70/1.10 uri_owl_sameAs ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (448) {G1,W9,D2,L2,V1,M1} R(77,7) { iext( X, uri_rdf__3, uri_rdf_Property )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (447) {G1,W9,D2,L2,V1,M1} R(77,86) { iext( X, uri_ex_Clique, uri_owl_Class
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (446) {G1,W9,D2,L2,V1,M1} R(77,84) { iext( X, uri_rdf_value,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (445) {G1,W9,D2,L2,V1,M1} R(77,83) { iext( X, uri_rdf_value,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (444) {G1,W9,D2,L2,V1,M1} R(77,8) { iext( X, uri_rdf_object,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (443) {G1,W9,D2,L2,V1,M1} R(77,82) { iext( X, uri_rdf_type, uri_rdfs_Class
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (442) {G1,W9,D2,L2,V1,M1} R(77,81) { iext( X, uri_rdf_type,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (441) {G1,W9,D2,L2,V1,M1} R(77,78) { iext( X, uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (440) {G1,W9,D2,L2,V1,M1} R(77,9) { iext( X, uri_rdf_value,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (439) {G1,W9,D2,L2,V1,M1} R(77,74) { iext( X, uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (438) {G1,W9,D2,L2,V1,M1} R(77,71) { iext( X, uri_rdfs_subClassOf,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (437) {G1,W9,D2,L2,V1,M1} R(77,67) { iext( X, uri_rdfs_subClassOf,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (436) {G1,W9,D2,L2,V1,M1} R(77,66) { iext( X, uri_rdf_subject,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (435) {G1,W9,D2,L2,V1,M1} R(77,10) { iext( X, uri_rdf_subject,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (434) {G1,W9,D2,L2,V1,M1} R(77,65) { iext( X, uri_rdf_subject,
% 0.70/1.10 uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.70/1.10 ) }.
% 0.70/1.10 (433) {G1,W9,D2,L2,V1,M1} R(77,64) { iext( X, uri_rdf_predicate,
% 0.70/1.10 uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.70/1.10 ) }.
% 0.70/1.10 (432) {G1,W9,D2,L2,V1,M1} R(77,63) { iext( X, uri_rdf_predicate,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (431) {G1,W9,D2,L2,V1,M1} R(77,62) { iext( X, uri_rdf_object,
% 0.70/1.10 uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.70/1.10 ) }.
% 0.70/1.10 (430) {G3,W9,D2,L2,V1,M1} R(77,125) { iext( X, uri_rdfs_domain,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (429) {G3,W9,D2,L2,V1,M1} R(77,126) { iext( X, uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (428) {G1,W9,D2,L2,V1,M1} R(77,13) { iext( X, uri_rdf_type,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (427) {G3,W9,D2,L2,V1,M1} R(77,127) { iext( X, uri_rdfs_range,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (426) {G3,W9,D2,L2,V1,M1} R(77,128) { iext( X, uri_rdfs_subClassOf,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (425) {G3,W9,D2,L2,V1,M1} R(77,129) { iext( X, uri_owl_onProperty,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (424) {G3,W9,D2,L2,V1,M1} R(77,130) { iext( X, uri_owl_someValuesFrom,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (423) {G1,W9,D2,L2,V1,M1} R(77,14) { iext( X, uri_rdfs_comment,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (422) {G3,W9,D2,L2,V1,M1} R(77,131) { iext( X, uri_owl_propertyChainAxiom,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (421) {G3,W9,D2,L2,V1,M1} R(77,132) { iext( X, uri_owl_inverseOf,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (420) {G1,W9,D2,L2,V1,M1} R(77,61) { iext( X, uri_rdfs_range,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (419) {G1,W9,D2,L2,V1,M1} R(77,59) { iext( X, uri_rdfs_range,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (418) {G1,W9,D2,L2,V1,M1} R(77,15) { iext( X, uri_rdfs_comment,
% 0.70/1.10 uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (417) {G1,W9,D2,L2,V1,M1} R(77,58) { iext( X, uri_rdf_Property,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (416) {G1,W9,D2,L2,V1,M1} R(77,52) { iext( X, uri_rdfs_domain,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (415) {G1,W9,D2,L2,V1,M1} R(77,50) { iext( X, uri_rdfs_domain,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (414) {G1,W9,D2,L2,V1,M1} R(77,49) { iext( X, uri_rdfs_Datatype,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X
% 0.70/1.10 ) }.
% 0.70/1.10 (413) {G1,W9,D2,L2,V1,M1} R(77,16) { iext( X, uri_rdfs_isDefinedBy,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (412) {G1,W9,D2,L2,V1,M1} R(77,47) { iext( X, uri_rdf_XMLLiteral,
% 0.70/1.10 uri_rdfs_Datatype ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X )
% 0.70/1.10 }.
% 0.70/1.10 (411) {G1,W9,D2,L2,V1,M1} R(77,46) { iext( X, uri_rdf_XMLLiteral,
% 0.70/1.10 uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf,
% 0.70/1.10 X ) }.
% 0.70/1.10 (410) {G1,W9,D2,L2,V1,M1} R(77,45) { iext( X, uri_rdfs_Seq,
% 0.70/1.10 uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (409) {G1,W9,D2,L2,V1,M1} R(77,44) { iext( X, uri_rdf__3,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_type, X ) }.
% 0.70/1.10 (408) {G1,W9,D2,L2,V1,M1} R(77,17) { iext( X, uri_rdfs_isDefinedBy,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (407) {G1,W9,D2,L2,V1,M1} R(77,43) { iext( X, uri_rdf__2,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_type, X ) }.
% 0.70/1.10 (406) {G1,W9,D2,L2,V1,M1} R(77,42) { iext( X, uri_rdf__1,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdf_type, X ) }.
% 0.70/1.10 (405) {G1,W9,D2,L2,V1,M1} R(77,41) { iext( X, uri_rdf__3, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (404) {G1,W9,D2,L2,V1,M1} R(77,40) { iext( X, uri_rdf__2, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (403) {G1,W9,D2,L2,V1,M1} R(77,18) { iext( X, uri_rdfs_isDefinedBy,
% 0.70/1.10 uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (402) {G1,W9,D2,L2,V1,M1} R(77,39) { iext( X, uri_rdf__1, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (401) {G1,W9,D2,L2,V1,M1} R(77,38) { iext( X, uri_rdf__3, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.70/1.10 (474) {G4,W9,D2,L2,V1,M1} R(473,77) { iext( X, uri_rdf_Alt, uri_rdfs_Class
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (497) {G3,W9,D2,L2,V1,M1} R(475,77) { iext( X, uri_ex_sameCliqueAs,
% 0.70/1.10 uri_ex_sameCliqueAs ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (400) {G1,W9,D2,L2,V1,M1} R(77,37) { iext( X, uri_rdf__2, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.70/1.10 (499) {G3,W9,D2,L2,V1,M1} R(476,77) { iext( X, uri_rdfs_isDefinedBy,
% 0.70/1.10 uri_rdfs_isDefinedBy ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (501) {G3,W9,D2,L2,V1,M1} R(477,77) { iext( X, uri_owl_sameAs,
% 0.70/1.10 uri_owl_sameAs ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (503) {G3,W9,D2,L2,V1,M1} R(478,77) { iext( X, uri_rdfs_seeAlso,
% 0.70/1.10 uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (509) {G1,W9,D2,L2,V1,M1} R(80,87) { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_owl_sameAs ), ! iext( uri_rdfs_subPropertyOf, X, uri_ex_sameCliqueAs
% 0.70/1.10 ) }.
% 0.70/1.10 (399) {G1,W9,D2,L2,V1,M1} R(77,36) { iext( X, uri_rdf__1, uri_rdfs_Resource
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.70/1.10 (508) {G1,W9,D2,L2,V1,M1} R(80,18) { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_rdfs_isDefinedBy ) }.
% 0.70/1.10 (507) {G3,W9,D2,L2,V1,M1} R(80,163) { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__3 ) }.
% 0.70/1.10 (506) {G3,W9,D2,L2,V1,M1} R(80,164) { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__2 ) }.
% 0.70/1.10 (505) {G3,W9,D2,L2,V1,M1} R(80,165) { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.10 uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__1 ) }.
% 0.70/1.10 (398) {G1,W9,D2,L2,V1,M1} R(77,19) { iext( X, uri_rdfs_label,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (510) {G5,W9,D2,L2,V1,M1} R(479,77) { iext( X, uri_rdfs_member,
% 0.70/1.10 uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (512) {G3,W9,D2,L2,V1,M1} R(480,77) { iext( X, uri_rdf__1, uri_rdf__1 ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (514) {G3,W9,D2,L2,V1,M1} R(481,77) { iext( X, uri_rdf__2, uri_rdf__2 ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (516) {G3,W9,D2,L2,V1,M1} R(482,77) { iext( X, uri_rdf__3, uri_rdf__3 ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (397) {G1,W9,D2,L2,V1,M1} R(77,35) { iext( X, uri_rdfs_member,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (518) {G3,W9,D2,L2,V1,M1} R(483,77) { iext( X, uri_rdf_object,
% 0.70/1.10 uri_rdf_object ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (521) {G3,W9,D2,L2,V1,M1} R(484,77) { iext( X, uri_rdf_value, uri_rdf_value
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (524) {G3,W9,D2,L2,V1,M1} R(485,77) { iext( X, uri_rdf_subject,
% 0.70/1.10 uri_rdf_subject ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (527) {G3,W9,D2,L2,V1,M1} R(486,77) { iext( X, uri_rdfs_domain,
% 0.70/1.10 uri_rdfs_domain ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (396) {G1,W9,D2,L2,V1,M1} R(77,34) { iext( X, uri_rdfs_member,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (530) {G3,W9,D2,L2,V1,M1} R(487,77) { iext( X, uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (533) {G3,W9,D2,L2,V1,M1} R(488,77) { iext( X, uri_rdfs_range,
% 0.70/1.10 uri_rdfs_range ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (536) {G3,W9,D2,L2,V1,M1} R(489,77) { iext( X, uri_rdfs_subClassOf,
% 0.70/1.10 uri_rdfs_subClassOf ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (539) {G3,W9,D2,L2,V1,M1} R(490,77) { iext( X, uri_owl_onProperty,
% 0.70/1.10 uri_owl_onProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (395) {G1,W9,D2,L2,V1,M1} R(77,33) { iext( X,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty, uri_rdf_Property ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (542) {G3,W9,D2,L2,V1,M1} R(491,77) { iext( X, uri_owl_someValuesFrom,
% 0.70/1.10 uri_owl_someValuesFrom ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (545) {G3,W9,D2,L2,V1,M1} R(492,77) { iext( X, uri_owl_propertyChainAxiom,
% 0.70/1.10 uri_owl_propertyChainAxiom ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (548) {G3,W9,D2,L2,V1,M1} R(493,77) { iext( X, uri_rdf_first, uri_rdf_first
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (551) {G3,W9,D2,L2,V1,M1} R(494,77) { iext( X, uri_rdf_rest, uri_rdf_rest )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (394) {G1,W9,D2,L2,V1,M1} R(77,31) { iext( X, uri_rdf_Bag,
% 0.70/1.10 uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (555) {G3,W9,D2,L2,V1,M1} R(495,77) { iext( X, uri_owl_inverseOf,
% 0.70/1.10 uri_owl_inverseOf ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (558) {G3,W9,D2,L2,V1,M1} R(496,77) { iext( X, uri_rdf_type, uri_rdf_type )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (561) {G4,W9,D2,L2,V1,M1} R(472,77) { iext( X, uri_rdf_Bag, uri_rdfs_Class
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (562) {G4,W9,D2,L2,V1,M1} R(379,77) { iext( X,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (393) {G1,W9,D2,L2,V1,M1} R(77,20) { iext( X, uri_rdfs_label,
% 0.70/1.10 uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (563) {G4,W9,D2,L2,V1,M1} R(378,77) { iext( X, uri_rdfs_Seq, uri_rdfs_Class
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (564) {G3,W9,D2,L2,V1,M1} R(377,77) { iext( X, uri_ex_sameCliqueAs,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (566) {G3,W9,D2,L2,V1,M1} R(376,77) { iext( X, uri_rdfs_isDefinedBy,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (568) {G7,W9,D2,L2,V1,M1} R(373,77) { iext( X, uri_rdfs_Resource,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (392) {G1,W9,D2,L2,V1,M1} R(77,30) { iext( X, uri_rdf_Alt,
% 0.70/1.10 uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (569) {G4,W9,D2,L2,V1,M1} R(372,77) { iext( X, uri_rdfs_Container,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (570) {G4,W9,D2,L2,V1,M1} R(371,77) { iext( X, uri_rdfs_Literal,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (571) {G4,W9,D2,L2,V1,M1} R(370,77) { iext( X, uri_rdfs_Class,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (572) {G4,W9,D2,L2,V1,M1} R(361,77) { iext( X, skol1, uri_rdfs_Class ), !
% 0.70/1.10 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (391) {G1,W9,D2,L2,V1,M1} R(77,29) { iext( X, uri_rdf_rest, uri_rdf_List )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.70/1.10 (573) {G4,W9,D2,L2,V1,M1} R(360,77) { iext( X, uri_rdf_XMLLiteral,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (574) {G4,W9,D2,L2,V1,M1} R(359,77) { iext( X, uri_rdfs_Datatype,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (575) {G4,W9,D2,L2,V1,M1} R(358,77) { iext( X, uri_ex_Clique,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (576) {G3,W9,D2,L2,V1,M1} R(346,77) { iext( X, uri_ex_Clique, uri_ex_Clique
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (390) {G1,W9,D2,L2,V1,M1} R(77,28) { iext( X, uri_rdf_rest, uri_rdf_List )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.70/1.10 (578) {G3,W9,D2,L2,V1,M1} R(347,77) { iext( X, uri_rdfs_Datatype,
% 0.70/1.10 uri_rdfs_Datatype ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (580) {G3,W9,D2,L2,V1,M1} R(348,77) { iext( X, uri_rdf_XMLLiteral,
% 0.70/1.10 uri_rdf_XMLLiteral ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (582) {G3,W9,D2,L2,V1,M1} R(349,77) { iext( X, skol1, skol1 ), ! iext(
% 0.70/1.10 uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (584) {G3,W9,D2,L2,V1,M1} R(350,77) { iext( X, uri_rdfs_Class,
% 0.70/1.10 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X
% 0.70/1.10 ) }.
% 0.70/1.10 (389) {G1,W9,D2,L2,V1,M1} R(77,27) { iext( X, uri_rdf_first,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (586) {G3,W9,D2,L2,V1,M1} R(351,77) { iext( X, uri_rdfs_Literal,
% 0.70/1.10 uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf,
% 0.70/1.10 X ) }.
% 0.70/1.10 (588) {G3,W9,D2,L2,V1,M1} R(352,77) { iext( X, uri_rdfs_Container,
% 0.70/1.10 uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (590) {G3,W9,D2,L2,V1,M1} R(353,77) { iext( X, uri_rdfs_Seq, uri_rdfs_Seq )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (592) {G3,W9,D2,L2,V1,M1} R(354,77) { iext( X,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty,
% 0.70/1.10 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.10 uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (388) {G1,W9,D2,L2,V1,M1} R(77,21) { iext( X, uri_rdfs_seeAlso,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.70/1.10 }.
% 0.70/1.10 (594) {G3,W9,D2,L2,V1,M1} R(355,77) { iext( X, uri_rdf_Bag, uri_rdf_Bag ),
% 0.70/1.10 ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (598) {G4,W9,D2,L2,V1,M1} R(597,77) { iext( X, uri_rdfs_label,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.10 (601) {G6,W9,D2,L2,V1,M1} R(600,77) { iext( X, uri_rdfs_label,
% 0.70/1.10 uri_rdfs_label ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (604) {G3,W9,D2,L2,V1,M1} R(356,77) { iext( X, uri_rdf_Alt, uri_rdf_Alt ),
% 0.70/1.10 ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (387) {G1,W9,D2,L2,V1,M1} R(77,26) { iext( X, uri_rdf_first, uri_rdf_List )
% 0.70/1.10 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.70/1.10 (606) {G4,W9,D2,L2,V1,M1} R(357,77) { iext( X, uri_rdf_Property,
% 0.70/1.10 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf,
% 0.70/1.10 X ) }.
% 0.70/1.10 (608) {G3,W9,D2,L2,V1,M1} R(345,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_ex_Clique ) }.
% 0.70/1.10 (607) {G3,W9,D2,L2,V1,M1} R(345,77) { iext( X, uri_ex_Clique,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (610) {G3,W9,D2,L2,V1,M1} R(343,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Datatype )
% 0.70/1.10 }.
% 0.70/1.10 (386) {G1,W9,D2,L2,V1,M1} R(77,22) { iext( X, uri_rdfs_seeAlso,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.70/1.10 }.
% 0.70/1.10 (609) {G3,W9,D2,L2,V1,M1} R(343,77) { iext( X, uri_rdfs_Datatype,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (612) {G3,W9,D2,L2,V1,M1} R(341,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral )
% 0.70/1.10 }.
% 0.70/1.10 (611) {G3,W9,D2,L2,V1,M1} R(341,77) { iext( X, uri_rdf_XMLLiteral,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (614) {G3,W9,D2,L2,V1,M1} R(339,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, skol1 ) }.
% 0.70/1.10 (384) {G4,W9,D2,L2,V1,M1} R(77,249) { iext( X, uri_rdf_Property,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (613) {G3,W9,D2,L2,V1,M1} R(339,77) { iext( X, skol1, uri_rdfs_Resource ),
% 0.70/1.10 ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.10 (616) {G3,W9,D2,L2,V1,M1} R(330,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Class ) }.
% 0.70/1.10 (615) {G3,W9,D2,L2,V1,M1} R(330,77) { iext( X, uri_rdfs_Class,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (618) {G3,W9,D2,L2,V1,M1} R(328,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Literal )
% 0.70/1.10 }.
% 0.70/1.10 (383) {G3,W9,D2,L2,V1,M1} R(77,163) { iext( X, uri_rdf__3, uri_rdfs_member
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (617) {G3,W9,D2,L2,V1,M1} R(328,77) { iext( X, uri_rdfs_Literal,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (621) {G3,W9,D2,L2,V1,M1} R(326,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Container )
% 0.70/1.10 }.
% 0.70/1.10 (620) {G3,W9,D2,L2,V1,M1} R(326,77) { iext( X, uri_rdfs_Container,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (622) {G6,W9,D2,L2,V1,M1} R(324,77) { iext( X, uri_rdfs_Resource,
% 0.70/1.10 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.10 , X ) }.
% 0.70/1.10 (382) {G3,W9,D2,L2,V1,M1} R(77,164) { iext( X, uri_rdf__2, uri_rdfs_member
% 0.70/1.10 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.10 (625) {G3,W9,D2,L2,V1,M1} R(317,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Seq ) }.
% 0.70/1.11 (624) {G3,W9,D2,L2,V1,M1} R(317,77) { iext( X, uri_rdfs_Seq,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (627) {G3,W9,D2,L2,V1,M1} R(315,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (626) {G3,W9,D2,L2,V1,M1} R(315,77) { iext( X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource ), ! iext(
% 0.70/1.11 uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (381) {G3,W9,D2,L2,V1,M1} R(77,165) { iext( X, uri_rdf__1, uri_rdfs_member
% 0.70/1.11 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (629) {G3,W9,D2,L2,V1,M1} R(313,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Bag ) }.
% 0.70/1.11 (628) {G3,W9,D2,L2,V1,M1} R(313,77) { iext( X, uri_rdf_Bag,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (631) {G3,W9,D2,L2,V1,M1} R(311,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Alt ) }.
% 0.70/1.11 (630) {G3,W9,D2,L2,V1,M1} R(311,77) { iext( X, uri_rdf_Alt,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (380) {G3,W9,D2,L2,V1,M1} R(77,301) { iext( X, uri_owl_sameAs,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (632) {G3,W9,D2,L2,V1,M1} R(300,77) { iext( X, uri_rdfs_seeAlso,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (633) {G5,W9,D2,L2,V1,M1} R(299,77) { iext( X, uri_rdfs_member,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (636) {G4,W9,D2,L2,V1,M1} R(635,77) { iext( X, uri_ex_JoesGang, skol1 ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (643) {G5,W9,D2,L2,V1,M1} R(641,77) { iext( X, uri_rdf_List, uri_rdf_List )
% 0.70/1.11 , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (369) {G1,W9,D2,L2,V1,M1} R(73,89) { iext( uri_rdfs_subClassOf, X, skol1 )
% 0.70/1.11 , ! iext( uri_rdfs_subClassOf, X, uri_ex_Clique ) }.
% 0.70/1.11 (647) {G5,W9,D2,L2,V1,M1} R(642,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_List ) }.
% 0.70/1.11 (646) {G5,W9,D2,L2,V1,M1} R(642,77) { iext( X, uri_rdf_List,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (648) {G4,W9,D2,L2,V1,M1} R(640,77) { iext( X, uri_rdf_List, uri_rdfs_Class
% 0.70/1.11 ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (651) {G4,W9,D2,L2,V1,M1} R(650,77) { iext( X, uri_rdfs_comment,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (368) {G1,W9,D2,L2,V1,M1} R(73,49) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Datatype ) }.
% 0.70/1.11 (654) {G6,W9,D2,L2,V1,M1} R(653,77) { iext( X, uri_rdfs_comment,
% 0.70/1.11 uri_rdfs_comment ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (662) {G5,W9,D2,L2,V1,M1} R(660,77) { iext( X, uri_rdfs_Statement,
% 0.70/1.11 uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (666) {G5,W9,D2,L2,V1,M1} R(661,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Statement )
% 0.70/1.11 }.
% 0.70/1.11 (665) {G5,W9,D2,L2,V1,M1} R(661,77) { iext( X, uri_rdfs_Statement,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (367) {G1,W9,D2,L2,V1,M1} R(73,46) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Literal ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral )
% 0.70/1.11 }.
% 0.70/1.11 (667) {G4,W9,D2,L2,V1,M1} R(659,77) { iext( X, uri_rdfs_Statement,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (673) {G5,W9,D2,L2,V1,M1} R(671,77) { iext( X, uri_owl_Class, uri_owl_Class
% 0.70/1.11 ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (677) {G5,W9,D2,L2,V1,M1} R(672,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_owl_Class ) }.
% 0.70/1.11 (676) {G5,W9,D2,L2,V1,M1} R(672,77) { iext( X, uri_owl_Class,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (366) {G1,W9,D2,L2,V1,M1} R(73,45) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Seq ) }.
% 0.70/1.11 (678) {G4,W9,D2,L2,V1,M1} R(670,77) { iext( X, uri_owl_Class,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (684) {G5,W9,D2,L2,V1,M1} R(682,77) { iext( X, uri_owl_Restriction,
% 0.70/1.11 uri_owl_Restriction ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (688) {G5,W9,D2,L2,V1,M1} R(683,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_owl_Restriction
% 0.70/1.11 ) }.
% 0.70/1.11 (687) {G5,W9,D2,L2,V1,M1} R(683,77) { iext( X, uri_owl_Restriction,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (365) {G1,W9,D2,L2,V1,M1} R(73,33) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (689) {G4,W9,D2,L2,V1,M1} R(681,77) { iext( X, uri_owl_Restriction,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (695) {G5,W9,D2,L2,V1,M1} R(693,77) { iext( X, uri_owl_ObjectProperty,
% 0.70/1.11 uri_owl_ObjectProperty ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (699) {G5,W9,D2,L2,V1,M1} R(694,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_owl_ObjectProperty ) }.
% 0.70/1.11 (698) {G5,W9,D2,L2,V1,M1} R(694,77) { iext( X, uri_owl_ObjectProperty,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (364) {G1,W9,D2,L2,V1,M1} R(73,31) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Bag ) }.
% 0.70/1.11 (700) {G4,W9,D2,L2,V1,M1} R(692,77) { iext( X, uri_owl_ObjectProperty,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (703) {G4,W9,D2,L2,V1,M1} R(702,77) { iext( X, uri_rdf_predicate,
% 0.70/1.11 uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (706) {G6,W9,D2,L2,V1,M1} R(705,77) { iext( X, uri_rdf_predicate,
% 0.70/1.11 uri_rdf_predicate ), ! iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (711) {G4,W9,D2,L2,V1,M1} R(710,77) { iext( X, skol3, uri_rdf_List ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (363) {G1,W9,D2,L2,V1,M1} R(73,30) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Alt ) }.
% 0.70/1.11 (714) {G4,W9,D2,L2,V1,M1} R(713,77) { iext( X, skol4, uri_rdf_List ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (720) {G5,W9,D2,L2,V1,M1} R(718,77) { iext( X, uri_ex_JoesGang,
% 0.70/1.11 uri_ex_JoesGang ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X
% 0.70/1.11 ) }.
% 0.70/1.11 (724) {G5,W9,D2,L2,V1,M1} R(719,73) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_ex_JoesGang )
% 0.70/1.11 }.
% 0.70/1.11 (723) {G5,W9,D2,L2,V1,M1} R(719,77) { iext( X, uri_ex_JoesGang,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.70/1.11 , X ) }.
% 0.70/1.11 (362) {G4,W9,D2,L2,V1,M1} R(73,249) { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Property )
% 0.70/1.11 }.
% 0.70/1.11 (725) {G4,W9,D2,L2,V1,M1} R(717,77) { iext( X, uri_ex_JoesGang,
% 0.70/1.11 uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (728) {G4,W9,D2,L2,V1,M1} R(727,77) { iext( X, skol2, uri_rdf_List ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (385) {G3,W9,D2,L2,V2,M1} R(77,162) { iext( X, Y, uri_rdfs_Resource ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.70/1.11 (244) {G1,W8,D2,L2,V1,M1} R(51,101) { icext( X, skol5 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_owl_inverseOf, X ) }.
% 0.70/1.11 (243) {G1,W8,D2,L2,V1,M1} R(51,100) { icext( X, skol4 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_rest, X ) }.
% 0.70/1.11 (241) {G1,W8,D2,L2,V1,M1} R(51,99) { icext( X, skol4 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_first, X ) }.
% 0.70/1.11 (240) {G1,W8,D2,L2,V1,M1} R(51,98) { icext( X, skol3 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_rest, X ) }.
% 0.70/1.11 (238) {G1,W8,D2,L2,V1,M1} R(51,97) { icext( X, skol3 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_first, X ) }.
% 0.70/1.11 (727) {G3,W4,D2,L1,V0,M1} R(726,24) { iext( uri_rdf_type, skol2,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (237) {G1,W8,D2,L2,V1,M1} R(51,96) { icext( X, skol2 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_rest, X ) }.
% 0.70/1.11 (726) {G2,W3,D2,L1,V0,M1} R(236,26) { icext( uri_rdf_List, skol2 ) }.
% 0.70/1.11 (236) {G1,W8,D2,L2,V1,M1} R(51,95) { icext( X, skol2 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_first, X ) }.
% 0.70/1.11 (235) {G1,W8,D2,L2,V1,M1} R(51,94) { icext( X, uri_foaf_knows ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_owl_propertyChainAxiom, X ) }.
% 0.70/1.11 (232) {G1,W8,D2,L2,V1,M1} R(51,92) { icext( X, skol1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_owl_someValuesFrom, X ) }.
% 0.70/1.11 (231) {G1,W8,D2,L2,V1,M1} R(51,91) { icext( X, skol1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_owl_onProperty, X ) }.
% 0.70/1.11 (229) {G1,W8,D2,L2,V1,M1} R(51,89) { icext( X, uri_ex_Clique ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (228) {G1,W8,D2,L2,V1,M1} R(51,88) { icext( X, uri_ex_sameCliqueAs ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (227) {G1,W8,D2,L2,V1,M1} R(51,87) { icext( X, uri_ex_sameCliqueAs ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (225) {G1,W8,D2,L2,V1,M1} R(51,84) { icext( X, uri_rdf_value ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (224) {G1,W8,D2,L2,V1,M1} R(51,83) { icext( X, uri_rdf_value ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (222) {G1,W8,D2,L2,V1,M1} R(51,82) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (221) {G1,W8,D2,L2,V1,M1} R(51,81) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (220) {G1,W8,D2,L2,V1,M1} R(51,78) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (251) {G4,W8,D2,L2,V1,M1} R(249,51) { icext( X, uri_rdf_Property ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (252) {G3,W8,D2,L2,V1,M1} R(163,51) { icext( X, uri_rdf__3 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (253) {G3,W8,D2,L2,V1,M1} R(164,51) { icext( X, uri_rdf__2 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (254) {G3,W8,D2,L2,V1,M1} R(165,51) { icext( X, uri_rdf__1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (722) {G5,W8,D2,L2,V1,M1} R(718,51) { icext( X, uri_ex_JoesGang ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (218) {G1,W8,D2,L2,V1,M1} R(51,74) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (721) {G5,W8,D2,L2,V1,M1} R(718,60) { icext( X, uri_ex_JoesGang ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (717) {G3,W4,D2,L1,V0,M1} R(715,24) { iext( uri_rdf_type, uri_ex_JoesGang,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (719) {G4,W4,D2,L1,V0,M1} R(716,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_ex_JoesGang, uri_rdfs_Resource ) }.
% 0.70/1.11 (718) {G4,W4,D2,L1,V0,M1} R(716,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_ex_JoesGang, uri_ex_JoesGang ) }.
% 0.70/1.11 (217) {G1,W8,D2,L2,V1,M1} R(51,71) { icext( X, uri_rdfs_subClassOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (716) {G3,W2,D2,L1,V0,M1} R(715,54) { ic( uri_ex_JoesGang ) }.
% 0.70/1.11 (715) {G2,W3,D2,L1,V0,M1} R(298,82) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_ex_JoesGang ) }.
% 0.70/1.11 (298) {G1,W8,D2,L2,V1,M1} R(60,103) { icext( X, uri_ex_JoesGang ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (297) {G1,W8,D2,L2,V1,M1} R(60,102) { icext( X, uri_ex_Clique ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (216) {G1,W8,D2,L2,V1,M1} R(51,67) { icext( X, uri_rdfs_subClassOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (296) {G1,W8,D2,L2,V1,M1} R(60,101) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_owl_inverseOf, X ) }.
% 0.70/1.11 (295) {G1,W8,D2,L2,V1,M1} R(60,100) { icext( X, uri_rdf_nil ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_rest, X ) }.
% 0.70/1.11 (294) {G1,W8,D2,L2,V1,M1} R(60,99) { icext( X, skol5 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_first, X ) }.
% 0.70/1.11 (713) {G3,W4,D2,L1,V0,M1} R(712,24) { iext( uri_rdf_type, skol4,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (215) {G1,W8,D2,L2,V1,M1} R(51,66) { icext( X, uri_rdf_subject ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (712) {G2,W3,D2,L1,V0,M1} R(293,29) { icext( uri_rdf_List, skol4 ) }.
% 0.70/1.11 (293) {G1,W8,D2,L2,V1,M1} R(60,98) { icext( X, skol4 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_rest, X ) }.
% 0.70/1.11 (292) {G1,W8,D2,L2,V1,M1} R(60,3) { icext( X, uri_rdf_List ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (291) {G1,W8,D2,L2,V1,M1} R(60,97) { icext( X, uri_ex_sameCliqueAs ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdf_first, X ) }.
% 0.70/1.11 (710) {G3,W4,D2,L1,V0,M1} R(709,24) { iext( uri_rdf_type, skol3,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (709) {G2,W3,D2,L1,V0,M1} R(290,29) { icext( uri_rdf_List, skol3 ) }.
% 0.70/1.11 (290) {G1,W8,D2,L2,V1,M1} R(60,96) { icext( X, skol3 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_rest, X ) }.
% 0.70/1.11 (289) {G1,W8,D2,L2,V1,M1} R(60,95) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_first, X ) }.
% 0.70/1.11 (213) {G1,W8,D2,L2,V1,M1} R(51,65) { icext( X, uri_rdf_subject ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (288) {G1,W8,D2,L2,V1,M1} R(60,94) { icext( X, skol2 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_owl_propertyChainAxiom, X ) }.
% 0.70/1.11 (697) {G5,W8,D2,L2,V1,M1} R(693,51) { icext( X, uri_owl_ObjectProperty ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (708) {G6,W8,D2,L2,V1,M1} R(705,51) { icext( X, uri_rdf_predicate ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (707) {G6,W8,D2,L2,V1,M1} R(705,60) { icext( X, uri_rdf_predicate ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (212) {G1,W8,D2,L2,V1,M1} R(51,64) { icext( X, uri_rdf_predicate ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (705) {G5,W4,D2,L1,V0,M1} R(704,79) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_predicate, uri_rdf_predicate ) }.
% 0.70/1.11 (704) {G4,W2,D2,L1,V0,M1} R(702,11) { ip( uri_rdf_predicate ) }.
% 0.70/1.11 (702) {G3,W4,D2,L1,V0,M1} R(701,24) { iext( uri_rdf_type, uri_rdf_predicate
% 0.70/1.11 , uri_rdf_Property ) }.
% 0.70/1.11 (701) {G2,W3,D2,L1,V0,M1} R(211,59) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdf_predicate ) }.
% 0.70/1.11 (211) {G1,W8,D2,L2,V1,M1} R(51,63) { icext( X, uri_rdf_predicate ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (696) {G5,W8,D2,L2,V1,M1} R(693,60) { icext( X, uri_owl_ObjectProperty ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (692) {G3,W4,D2,L1,V0,M1} R(690,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_owl_ObjectProperty, uri_rdfs_Class ) }.
% 0.70/1.11 (694) {G4,W4,D2,L1,V0,M1} R(691,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_ObjectProperty, uri_rdfs_Resource ) }.
% 0.70/1.11 (693) {G4,W4,D2,L1,V0,M1} R(691,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_ObjectProperty, uri_owl_ObjectProperty ) }.
% 0.70/1.11 (210) {G1,W8,D2,L2,V1,M1} R(51,62) { icext( X, uri_rdf_object ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (691) {G3,W2,D2,L1,V0,M1} R(690,54) { ic( uri_owl_ObjectProperty ) }.
% 0.70/1.11 (690) {G2,W3,D2,L1,V0,M1} R(287,82) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_owl_ObjectProperty ) }.
% 0.70/1.11 (287) {G1,W8,D2,L2,V1,M1} R(60,93) { icext( X, uri_owl_ObjectProperty ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (286) {G1,W8,D2,L2,V1,M1} R(60,92) { icext( X, uri_ex_Clique ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_owl_someValuesFrom, X ) }.
% 0.70/1.11 (285) {G1,W8,D2,L2,V1,M1} R(60,91) { icext( X, uri_ex_sameCliqueAs ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_owl_onProperty, X ) }.
% 0.70/1.11 (686) {G5,W8,D2,L2,V1,M1} R(682,51) { icext( X, uri_owl_Restriction ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (685) {G5,W8,D2,L2,V1,M1} R(682,60) { icext( X, uri_owl_Restriction ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (681) {G3,W4,D2,L1,V0,M1} R(679,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_owl_Restriction, uri_rdfs_Class ) }.
% 0.70/1.11 (683) {G4,W4,D2,L1,V0,M1} R(680,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_Restriction, uri_rdfs_Resource ) }.
% 0.70/1.11 (682) {G4,W4,D2,L1,V0,M1} R(680,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_Restriction, uri_owl_Restriction ) }.
% 0.70/1.11 (680) {G3,W2,D2,L1,V0,M1} R(679,54) { ic( uri_owl_Restriction ) }.
% 0.70/1.11 (679) {G2,W3,D2,L1,V0,M1} R(284,82) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_owl_Restriction ) }.
% 0.70/1.11 (284) {G1,W8,D2,L2,V1,M1} R(60,90) { icext( X, uri_owl_Restriction ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (283) {G1,W8,D2,L2,V1,M1} R(60,89) { icext( X, skol1 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (282) {G1,W8,D2,L2,V1,M1} R(60,88) { icext( X, uri_ex_Clique ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (281) {G1,W8,D2,L2,V1,M1} R(60,87) { icext( X, uri_owl_sameAs ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (675) {G5,W8,D2,L2,V1,M1} R(671,51) { icext( X, uri_owl_Class ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (674) {G5,W8,D2,L2,V1,M1} R(671,60) { icext( X, uri_owl_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (670) {G3,W4,D2,L1,V0,M1} R(668,24) { iext( uri_rdf_type, uri_owl_Class,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (672) {G4,W4,D2,L1,V0,M1} R(669,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_Class, uri_rdfs_Resource ) }.
% 0.70/1.11 (671) {G4,W4,D2,L1,V0,M1} R(669,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_owl_Class, uri_owl_Class ) }.
% 0.70/1.11 (669) {G3,W2,D2,L1,V0,M1} R(668,54) { ic( uri_owl_Class ) }.
% 0.70/1.11 (668) {G2,W3,D2,L1,V0,M1} R(280,82) { icext( uri_rdfs_Class, uri_owl_Class
% 0.70/1.11 ) }.
% 0.70/1.11 (280) {G1,W8,D2,L2,V1,M1} R(60,86) { icext( X, uri_owl_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (279) {G1,W8,D2,L2,V1,M1} R(60,78) { icext( X, uri_rdf_Property ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (278) {G1,W8,D2,L2,V1,M1} R(60,67) { icext( X, uri_rdfs_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.70/1.11 (664) {G5,W8,D2,L2,V1,M1} R(660,51) { icext( X, uri_rdfs_Statement ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (663) {G5,W8,D2,L2,V1,M1} R(660,60) { icext( X, uri_rdfs_Statement ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (659) {G3,W4,D2,L1,V0,M1} R(657,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_Statement, uri_rdfs_Class ) }.
% 0.70/1.11 (661) {G4,W4,D2,L1,V0,M1} R(658,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Statement, uri_rdfs_Resource ) }.
% 0.70/1.11 (660) {G4,W4,D2,L1,V0,M1} R(658,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Statement, uri_rdfs_Statement ) }.
% 0.70/1.11 (658) {G3,W2,D2,L1,V0,M1} R(657,54) { ic( uri_rdfs_Statement ) }.
% 0.70/1.11 (202) {G1,W8,D2,L2,V1,M1} R(51,14) { icext( X, uri_rdfs_comment ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (657) {G2,W3,D2,L1,V0,M1} R(277,52) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Statement ) }.
% 0.70/1.11 (277) {G1,W8,D2,L2,V1,M1} R(60,62) { icext( X, uri_rdfs_Statement ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.70/1.11 (276) {G3,W8,D2,L2,V1,M1} R(60,132) { icext( X, uri_rdf_Property ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (275) {G1,W8,D2,L2,V1,M1} R(60,58) { icext( X, uri_rdfs_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (274) {G1,W8,D2,L2,V1,M1} R(60,52) { icext( X, uri_rdfs_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (273) {G1,W8,D2,L2,V1,M1} R(60,50) { icext( X, uri_rdf_Property ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.70/1.11 (272) {G1,W8,D2,L2,V1,M1} R(60,49) { icext( X, uri_rdfs_Class ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (271) {G1,W8,D2,L2,V1,M1} R(60,47) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (270) {G1,W8,D2,L2,V1,M1} R(60,46) { icext( X, uri_rdfs_Literal ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (269) {G1,W8,D2,L2,V1,M1} R(60,42) { icext( X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_range,
% 0.70/1.11 uri_rdf_type, X ) }.
% 0.70/1.11 (268) {G1,W8,D2,L2,V1,M1} R(60,18) { icext( X, uri_rdfs_seeAlso ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (267) {G1,W8,D2,L2,V1,M1} R(60,33) { icext( X, uri_rdf_Property ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (199) {G1,W8,D2,L2,V1,M1} R(51,61) { icext( X, uri_rdfs_range ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (266) {G1,W8,D2,L2,V1,M1} R(60,20) { icext( X, uri_rdfs_Literal ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (265) {G1,W8,D2,L2,V1,M1} R(60,30) { icext( X, uri_rdfs_Container ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (656) {G6,W8,D2,L2,V1,M1} R(653,51) { icext( X, uri_rdfs_comment ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (655) {G6,W8,D2,L2,V1,M1} R(653,60) { icext( X, uri_rdfs_comment ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (198) {G1,W8,D2,L2,V1,M1} R(51,59) { icext( X, uri_rdfs_range ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (653) {G5,W4,D2,L1,V0,M1} R(652,79) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_comment, uri_rdfs_comment ) }.
% 0.70/1.11 (652) {G4,W2,D2,L1,V0,M1} R(650,11) { ip( uri_rdfs_comment ) }.
% 0.70/1.11 (650) {G3,W4,D2,L1,V0,M1} R(649,24) { iext( uri_rdf_type, uri_rdfs_comment
% 0.70/1.11 , uri_rdf_Property ) }.
% 0.70/1.11 (649) {G2,W3,D2,L1,V0,M1} R(197,59) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_comment ) }.
% 0.70/1.11 (197) {G1,W8,D2,L2,V1,M1} R(51,15) { icext( X, uri_rdfs_comment ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (264) {G1,W8,D2,L2,V1,M1} R(60,29) { icext( X, uri_rdf_List ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (263) {G1,W8,D2,L2,V1,M1} R(60,21) { icext( X, uri_rdfs_Resource ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.70/1.11 (645) {G5,W8,D2,L2,V1,M1} R(641,51) { icext( X, uri_rdf_List ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (644) {G5,W8,D2,L2,V1,M1} R(641,60) { icext( X, uri_rdf_List ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (640) {G3,W4,D2,L1,V0,M1} R(638,24) { iext( uri_rdf_type, uri_rdf_List,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (642) {G4,W4,D2,L1,V0,M1} R(639,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_List, uri_rdfs_Resource ) }.
% 0.70/1.11 (641) {G4,W4,D2,L1,V0,M1} R(639,72) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_List, uri_rdf_List ) }.
% 0.70/1.11 (639) {G3,W2,D2,L1,V0,M1} R(638,54) { ic( uri_rdf_List ) }.
% 0.70/1.11 (195) {G1,W8,D2,L2,V1,M1} R(51,52) { icext( X, uri_rdfs_domain ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (638) {G2,W3,D2,L1,V0,M1} R(262,52) { icext( uri_rdfs_Class, uri_rdf_List )
% 0.70/1.11 }.
% 0.70/1.11 (262) {G1,W8,D2,L2,V1,M1} R(60,26) { icext( X, uri_rdf_List ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.70/1.11 (261) {G1,W8,D2,L2,V1,M1} R(60,22) { icext( X, uri_rdfs_Resource ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.70/1.11 (260) {G3,W8,D2,L2,V1,M1} R(60,162) { icext( X, uri_rdfs_Resource ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (194) {G1,W8,D2,L2,V1,M1} R(51,49) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (259) {G4,W8,D2,L2,V1,M1} R(60,249) { icext( X, uri_rdfs_Resource ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (258) {G3,W8,D2,L2,V1,M1} R(60,165) { icext( X, uri_rdfs_member ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (498) {G3,W8,D2,L2,V1,M1} R(475,60) { icext( X, uri_ex_sameCliqueAs ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (500) {G3,W8,D2,L2,V1,M1} R(476,60) { icext( X, uri_rdfs_isDefinedBy ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (193) {G1,W8,D2,L2,V1,M1} R(51,16) { icext( X, uri_rdfs_isDefinedBy ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (502) {G3,W8,D2,L2,V1,M1} R(477,51) { icext( X, uri_owl_sameAs ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (504) {G3,W8,D2,L2,V1,M1} R(478,51) { icext( X, uri_rdfs_seeAlso ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (511) {G5,W8,D2,L2,V1,M1} R(479,51) { icext( X, uri_rdfs_member ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (513) {G3,W8,D2,L2,V1,M1} R(480,60) { icext( X, uri_rdf__1 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (515) {G3,W8,D2,L2,V1,M1} R(481,60) { icext( X, uri_rdf__2 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (517) {G3,W8,D2,L2,V1,M1} R(482,60) { icext( X, uri_rdf__3 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (520) {G3,W8,D2,L2,V1,M1} R(483,51) { icext( X, uri_rdf_object ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (519) {G3,W8,D2,L2,V1,M1} R(483,60) { icext( X, uri_rdf_object ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (191) {G1,W8,D2,L2,V1,M1} R(51,46) { icext( X, uri_rdf_XMLLiteral ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (523) {G3,W8,D2,L2,V1,M1} R(484,51) { icext( X, uri_rdf_value ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (522) {G3,W8,D2,L2,V1,M1} R(484,60) { icext( X, uri_rdf_value ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (526) {G3,W8,D2,L2,V1,M1} R(485,51) { icext( X, uri_rdf_subject ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (525) {G3,W8,D2,L2,V1,M1} R(485,60) { icext( X, uri_rdf_subject ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (190) {G1,W8,D2,L2,V1,M1} R(51,45) { icext( X, uri_rdfs_Seq ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (529) {G3,W8,D2,L2,V1,M1} R(486,51) { icext( X, uri_rdfs_domain ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (528) {G3,W8,D2,L2,V1,M1} R(486,60) { icext( X, uri_rdfs_domain ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (532) {G3,W8,D2,L2,V1,M1} R(487,51) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (531) {G3,W8,D2,L2,V1,M1} R(487,60) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (535) {G3,W8,D2,L2,V1,M1} R(488,51) { icext( X, uri_rdfs_range ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (534) {G3,W8,D2,L2,V1,M1} R(488,60) { icext( X, uri_rdfs_range ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (538) {G3,W8,D2,L2,V1,M1} R(489,51) { icext( X, uri_rdfs_subClassOf ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (537) {G3,W8,D2,L2,V1,M1} R(489,60) { icext( X, uri_rdfs_subClassOf ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (188) {G1,W8,D2,L2,V1,M1} R(51,17) { icext( X, uri_rdfs_isDefinedBy ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (541) {G3,W8,D2,L2,V1,M1} R(490,51) { icext( X, uri_owl_onProperty ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (540) {G3,W8,D2,L2,V1,M1} R(490,60) { icext( X, uri_owl_onProperty ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (544) {G3,W8,D2,L2,V1,M1} R(491,51) { icext( X, uri_owl_someValuesFrom ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (543) {G3,W8,D2,L2,V1,M1} R(491,60) { icext( X, uri_owl_someValuesFrom ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (547) {G3,W8,D2,L2,V1,M1} R(492,51) { icext( X, uri_owl_propertyChainAxiom
% 0.70/1.11 ), ! iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (546) {G3,W8,D2,L2,V1,M1} R(492,60) { icext( X, uri_owl_propertyChainAxiom
% 0.70/1.11 ), ! iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (550) {G3,W8,D2,L2,V1,M1} R(493,51) { icext( X, uri_rdf_first ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (549) {G3,W8,D2,L2,V1,M1} R(493,60) { icext( X, uri_rdf_first ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (553) {G3,W8,D2,L2,V1,M1} R(494,51) { icext( X, uri_rdf_rest ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (552) {G3,W8,D2,L2,V1,M1} R(494,60) { icext( X, uri_rdf_rest ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (557) {G3,W8,D2,L2,V1,M1} R(495,51) { icext( X, uri_owl_inverseOf ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (556) {G3,W8,D2,L2,V1,M1} R(495,60) { icext( X, uri_owl_inverseOf ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (185) {G1,W8,D2,L2,V1,M1} R(51,41) { icext( X, uri_rdf__3 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (560) {G3,W8,D2,L2,V1,M1} R(496,51) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (559) {G3,W8,D2,L2,V1,M1} R(496,60) { icext( X, uri_rdf_type ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (577) {G3,W8,D2,L2,V1,M1} R(346,60) { icext( X, uri_ex_Clique ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (579) {G3,W8,D2,L2,V1,M1} R(347,60) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.70/1.11 ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (184) {G1,W8,D2,L2,V1,M1} R(51,40) { icext( X, uri_rdf__2 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (581) {G3,W8,D2,L2,V1,M1} R(348,60) { icext( X, uri_rdf_XMLLiteral ), !
% 0.70/1.11 iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (583) {G3,W8,D2,L2,V1,M1} R(349,51) { icext( X, skol1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (585) {G3,W8,D2,L2,V1,M1} R(350,51) { icext( X, uri_rdfs_Class ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (587) {G3,W8,D2,L2,V1,M1} R(351,51) { icext( X, uri_rdfs_Literal ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (183) {G1,W8,D2,L2,V1,M1} R(51,18) { icext( X, uri_rdfs_isDefinedBy ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (589) {G3,W8,D2,L2,V1,M1} R(352,51) { icext( X, uri_rdfs_Container ), !
% 0.70/1.11 iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (591) {G3,W8,D2,L2,V1,M1} R(353,60) { icext( X, uri_rdfs_Seq ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (593) {G3,W8,D2,L2,V1,M1} R(354,60) { icext( X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_range,
% 0.70/1.11 uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (595) {G3,W8,D2,L2,V1,M1} R(355,60) { icext( X, uri_rdf_Bag ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (182) {G1,W8,D2,L2,V1,M1} R(51,39) { icext( X, uri_rdf__1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (603) {G6,W8,D2,L2,V1,M1} R(600,51) { icext( X, uri_rdfs_label ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (602) {G6,W8,D2,L2,V1,M1} R(600,60) { icext( X, uri_rdfs_label ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (605) {G3,W8,D2,L2,V1,M1} R(356,60) { icext( X, uri_rdf_Alt ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (623) {G6,W8,D2,L2,V1,M1} R(324,51) { icext( X, uri_rdfs_Resource ), ! iext
% 0.70/1.11 ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (181) {G1,W8,D2,L2,V1,M1} R(51,38) { icext( X, uri_rdf__3 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (637) {G4,W8,D2,L2,V1,M1} R(635,60) { icext( X, skol1 ), ! iext(
% 0.70/1.11 uri_rdfs_range, uri_rdf_type, X ) }.
% 0.70/1.11 (250) {G3,W8,D2,L2,V2,M1} R(162,51) { icext( X, Y ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdf_type, X ) }.
% 0.70/1.11 (635) {G3,W4,D2,L1,V0,M1} R(634,24) { iext( uri_rdf_type, uri_ex_JoesGang,
% 0.70/1.11 skol1 ) }.
% 0.70/1.11 (634) {G2,W3,D2,L1,V0,M1} R(337,159) { icext( skol1, uri_ex_JoesGang ) }.
% 0.70/1.11 (180) {G1,W8,D2,L2,V1,M1} R(51,37) { icext( X, uri_rdf__2 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (337) {G1,W7,D2,L2,V1,M1} R(70,89) { icext( skol1, X ), ! icext(
% 0.70/1.11 uri_ex_Clique, X ) }.
% 0.70/1.11 (336) {G1,W7,D2,L2,V1,M1} R(70,49) { icext( uri_rdfs_Class, X ), ! icext(
% 0.70/1.11 uri_rdfs_Datatype, X ) }.
% 0.70/1.11 (335) {G1,W7,D2,L2,V1,M1} R(70,46) { icext( uri_rdfs_Literal, X ), ! icext
% 0.70/1.11 ( uri_rdf_XMLLiteral, X ) }.
% 0.70/1.11 (334) {G1,W7,D2,L2,V1,M1} R(70,45) { icext( uri_rdfs_Container, X ), !
% 0.70/1.11 icext( uri_rdfs_Seq, X ) }.
% 0.70/1.11 (179) {G1,W8,D2,L2,V1,M1} R(51,36) { icext( X, uri_rdf__1 ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (333) {G1,W7,D2,L2,V1,M1} R(70,33) { icext( uri_rdf_Property, X ), ! icext
% 0.70/1.11 ( uri_rdfs_ContainerMembershipProperty, X ) }.
% 0.70/1.11 (332) {G1,W7,D2,L2,V1,M1} R(70,31) { icext( uri_rdfs_Container, X ), !
% 0.70/1.11 icext( uri_rdf_Bag, X ) }.
% 0.70/1.11 (331) {G1,W7,D2,L2,V1,M1} R(70,30) { icext( uri_rdfs_Container, X ), !
% 0.70/1.11 icext( uri_rdf_Alt, X ) }.
% 0.70/1.11 (299) {G4,W4,D2,L1,V0,M1} R(255,12) { iext( uri_rdf_type, uri_rdfs_member,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (178) {G1,W8,D2,L2,V1,M1} R(51,19) { icext( X, uri_rdfs_label ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (300) {G2,W4,D2,L1,V0,M1} R(256,12) { iext( uri_rdf_type, uri_rdfs_seeAlso
% 0.70/1.11 , uri_rdf_Property ) }.
% 0.70/1.11 (311) {G2,W4,D2,L1,V0,M1} R(303,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Alt, uri_rdfs_Resource ) }.
% 0.70/1.11 (313) {G2,W4,D2,L1,V0,M1} R(304,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Bag, uri_rdfs_Resource ) }.
% 0.70/1.11 (315) {G2,W4,D2,L1,V0,M1} R(305,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource ) }.
% 0.70/1.11 (177) {G1,W8,D2,L2,V1,M1} R(51,35) { icext( X, uri_rdfs_member ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (317) {G2,W4,D2,L1,V0,M1} R(306,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Seq, uri_rdfs_Resource ) }.
% 0.70/1.11 (324) {G5,W4,D2,L1,V0,M1} R(318,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Resource, uri_rdfs_Resource ) }.
% 0.70/1.11 (326) {G2,W4,D2,L1,V0,M1} R(319,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Container, uri_rdfs_Resource ) }.
% 0.70/1.11 (619) {G2,W3,D2,L1,V0,M1} R(176,50) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_member ) }.
% 0.70/1.11 (176) {G1,W8,D2,L2,V1,M1} R(51,34) { icext( X, uri_rdfs_member ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (328) {G2,W4,D2,L1,V0,M1} R(320,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Literal, uri_rdfs_Resource ) }.
% 0.70/1.11 (330) {G2,W4,D2,L1,V0,M1} R(321,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Class, uri_rdfs_Resource ) }.
% 0.70/1.11 (339) {G2,W4,D2,L1,V0,M1} R(322,25) { iext( uri_rdfs_subClassOf, skol1,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (341) {G2,W4,D2,L1,V0,M1} R(307,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_XMLLiteral, uri_rdfs_Resource ) }.
% 0.70/1.11 (175) {G1,W8,D2,L2,V1,M1} R(51,33) { icext( X,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_domain,
% 0.70/1.11 uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (343) {G2,W4,D2,L1,V0,M1} R(308,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Datatype, uri_rdfs_Resource ) }.
% 0.70/1.11 (345) {G2,W4,D2,L1,V0,M1} R(309,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_ex_Clique, uri_rdfs_Resource ) }.
% 0.70/1.11 (357) {G3,W4,D2,L1,V0,M1} R(72,248) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Property, uri_rdf_Property ) }.
% 0.70/1.11 (356) {G2,W4,D2,L1,V0,M1} R(72,303) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Alt, uri_rdf_Alt ) }.
% 0.70/1.11 (174) {G1,W8,D2,L2,V1,M1} R(51,31) { icext( X, uri_rdf_Bag ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (600) {G5,W4,D2,L1,V0,M1} R(599,79) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_label, uri_rdfs_label ) }.
% 0.70/1.11 (599) {G4,W2,D2,L1,V0,M1} R(597,11) { ip( uri_rdfs_label ) }.
% 0.70/1.11 (597) {G3,W4,D2,L1,V0,M1} R(596,24) { iext( uri_rdf_type, uri_rdfs_label,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (596) {G2,W3,D2,L1,V0,M1} R(173,59) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_label ) }.
% 0.70/1.11 (173) {G1,W8,D2,L2,V1,M1} R(51,20) { icext( X, uri_rdfs_label ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (355) {G2,W4,D2,L1,V0,M1} R(72,304) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Bag, uri_rdf_Bag ) }.
% 0.70/1.11 (354) {G2,W4,D2,L1,V0,M1} R(72,305) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (353) {G2,W4,D2,L1,V0,M1} R(72,306) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Seq, uri_rdfs_Seq ) }.
% 0.70/1.11 (352) {G2,W4,D2,L1,V0,M1} R(72,319) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Container, uri_rdfs_Container ) }.
% 0.70/1.11 (172) {G1,W8,D2,L2,V1,M1} R(51,30) { icext( X, uri_rdf_Alt ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.70/1.11 (351) {G2,W4,D2,L1,V0,M1} R(72,320) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Literal, uri_rdfs_Literal ) }.
% 0.70/1.11 (350) {G2,W4,D2,L1,V0,M1} R(72,321) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Class, uri_rdfs_Class ) }.
% 0.70/1.11 (349) {G2,W4,D2,L1,V0,M1} R(72,322) { iext( uri_rdfs_subClassOf, skol1,
% 0.70/1.11 skol1 ) }.
% 0.70/1.11 (348) {G2,W4,D2,L1,V0,M1} R(72,307) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_XMLLiteral, uri_rdf_XMLLiteral ) }.
% 0.70/1.11 (171) {G1,W8,D2,L2,V1,M1} R(51,29) { icext( X, uri_rdf_rest ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (347) {G2,W4,D2,L1,V0,M1} R(72,308) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Datatype, uri_rdfs_Datatype ) }.
% 0.70/1.11 (346) {G2,W4,D2,L1,V0,M1} R(72,309) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_ex_Clique, uri_ex_Clique ) }.
% 0.70/1.11 (358) {G3,W4,D2,L1,V0,M1} R(344,24) { iext( uri_rdf_type, uri_ex_Clique,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (359) {G3,W4,D2,L1,V0,M1} R(342,24) { iext( uri_rdf_type, uri_rdfs_Datatype
% 0.70/1.11 , uri_rdfs_Class ) }.
% 0.70/1.11 (170) {G1,W8,D2,L2,V1,M1} R(51,28) { icext( X, uri_rdf_rest ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (360) {G3,W4,D2,L1,V0,M1} R(340,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdf_XMLLiteral, uri_rdfs_Class ) }.
% 0.70/1.11 (361) {G3,W4,D2,L1,V0,M1} R(338,24) { iext( uri_rdf_type, skol1,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (370) {G3,W4,D2,L1,V0,M1} R(329,24) { iext( uri_rdf_type, uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (371) {G3,W4,D2,L1,V0,M1} R(327,24) { iext( uri_rdf_type, uri_rdfs_Literal
% 0.70/1.11 , uri_rdfs_Class ) }.
% 0.70/1.11 (169) {G1,W8,D2,L2,V1,M1} R(51,27) { icext( X, uri_rdf_first ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (372) {G3,W4,D2,L1,V0,M1} R(325,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_Container, uri_rdfs_Class ) }.
% 0.70/1.11 (373) {G6,W4,D2,L1,V0,M1} R(323,24) { iext( uri_rdf_type, uri_rdfs_Resource
% 0.70/1.11 , uri_rdfs_Class ) }.
% 0.70/1.11 (567) {G3,W3,D2,L1,V0,M1} R(376,23) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_isDefinedBy ) }.
% 0.70/1.11 (376) {G2,W4,D2,L1,V0,M1} R(374,12) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_isDefinedBy, uri_rdf_Property ) }.
% 0.70/1.11 (168) {G1,W8,D2,L2,V1,M1} R(51,21) { icext( X, uri_rdfs_seeAlso ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (565) {G3,W3,D2,L1,V0,M1} R(377,23) { icext( uri_rdf_Property,
% 0.70/1.11 uri_ex_sameCliqueAs ) }.
% 0.70/1.11 (377) {G2,W4,D2,L1,V0,M1} R(375,12) { iext( uri_rdf_type,
% 0.70/1.11 uri_ex_sameCliqueAs, uri_rdf_Property ) }.
% 0.70/1.11 (378) {G3,W4,D2,L1,V0,M1} R(316,24) { iext( uri_rdf_type, uri_rdfs_Seq,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (379) {G3,W4,D2,L1,V0,M1} R(314,24) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class ) }.
% 0.70/1.11 (167) {G1,W8,D2,L2,V1,M1} R(51,26) { icext( X, uri_rdf_first ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (472) {G3,W4,D2,L1,V0,M1} R(312,24) { iext( uri_rdf_type, uri_rdf_Bag,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (496) {G2,W4,D2,L1,V0,M1} R(79,108) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_type, uri_rdf_type ) }.
% 0.70/1.11 (495) {G2,W4,D2,L1,V0,M1} R(79,109) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_owl_inverseOf, uri_owl_inverseOf ) }.
% 0.70/1.11 (554) {G2,W3,D2,L1,V0,M1} R(166,59) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_seeAlso ) }.
% 0.70/1.11 (166) {G1,W8,D2,L2,V1,M1} R(51,22) { icext( X, uri_rdfs_seeAlso ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.70/1.11 (494) {G2,W4,D2,L1,V0,M1} R(79,110) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_rest, uri_rdf_rest ) }.
% 0.70/1.11 (493) {G2,W4,D2,L1,V0,M1} R(79,111) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_first, uri_rdf_first ) }.
% 0.70/1.11 (492) {G2,W4,D2,L1,V0,M1} R(79,112) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom ) }.
% 0.70/1.11 (491) {G2,W4,D2,L1,V0,M1} R(79,113) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_owl_someValuesFrom, uri_owl_someValuesFrom ) }.
% 0.70/1.11 (107) {G1,W9,D2,L2,V1,M1} F(77) { iext( X, uri_rdfs_subPropertyOf, X ), !
% 0.70/1.11 iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.70/1.11 (490) {G2,W4,D2,L1,V0,M1} R(79,114) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_owl_onProperty, uri_owl_onProperty ) }.
% 0.70/1.11 (489) {G2,W4,D2,L1,V0,M1} R(79,115) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subClassOf, uri_rdfs_subClassOf ) }.
% 0.70/1.11 (488) {G2,W4,D2,L1,V0,M1} R(79,116) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_range, uri_rdfs_range ) }.
% 0.70/1.11 (487) {G2,W4,D2,L1,V0,M1} R(79,117) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf ) }.
% 0.70/1.11 (106) {G1,W8,D2,L2,V1,M1} F(60) { icext( X, X ), ! iext( uri_rdfs_range,
% 0.70/1.11 uri_rdfs_range, X ) }.
% 0.70/1.11 (486) {G2,W4,D2,L1,V0,M1} R(79,118) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain ) }.
% 0.70/1.11 (485) {G2,W4,D2,L1,V0,M1} R(79,119) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_subject, uri_rdf_subject ) }.
% 0.70/1.11 (484) {G2,W4,D2,L1,V0,M1} R(79,120) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_value, uri_rdf_value ) }.
% 0.70/1.11 (483) {G2,W4,D2,L1,V0,M1} R(79,121) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_object, uri_rdf_object ) }.
% 0.70/1.11 (105) {G1,W8,D2,L2,V1,M1} F(51) { icext( X, uri_rdfs_domain ), ! iext(
% 0.70/1.11 uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.70/1.11 (482) {G2,W4,D2,L1,V0,M1} R(79,122) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__3, uri_rdf__3 ) }.
% 0.70/1.11 (481) {G2,W4,D2,L1,V0,M1} R(79,123) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__2, uri_rdf__2 ) }.
% 0.70/1.11 (480) {G2,W4,D2,L1,V0,M1} R(79,124) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__1, uri_rdf__1 ) }.
% 0.70/1.11 (479) {G4,W4,D2,L1,V0,M1} R(79,255) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_member, uri_rdfs_member ) }.
% 0.70/1.11 (80) {G0,W14,D2,L3,V3,M1} I { ! iext( uri_rdfs_subPropertyOf, X, Z ), iext
% 0.70/1.11 ( uri_rdfs_subPropertyOf, X, Y ), ! iext( uri_rdfs_subPropertyOf, Z, Y )
% 0.70/1.11 }.
% 0.70/1.11 (478) {G2,W4,D2,L1,V0,M1} R(79,256) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_seeAlso, uri_rdfs_seeAlso ) }.
% 0.70/1.11 (477) {G2,W4,D2,L1,V0,M1} R(79,257) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_owl_sameAs, uri_owl_sameAs ) }.
% 0.70/1.11 (476) {G2,W4,D2,L1,V0,M1} R(79,374) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy ) }.
% 0.70/1.11 (475) {G2,W4,D2,L1,V0,M1} R(79,375) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_ex_sameCliqueAs, uri_ex_sameCliqueAs ) }.
% 0.70/1.11 (79) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subPropertyOf, X, X ), ! ip( X
% 0.70/1.11 ) }.
% 0.70/1.11 (473) {G3,W4,D2,L1,V0,M1} R(310,24) { iext( uri_rdf_type, uri_rdf_Alt,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (302) {G3,W3,D2,L1,V0,M1} R(301,23) { icext( uri_rdf_Property,
% 0.70/1.11 uri_owl_sameAs ) }.
% 0.70/1.11 (310) {G2,W3,D2,L1,V0,M1} R(303,53) { icext( uri_rdfs_Class, uri_rdf_Alt )
% 0.70/1.11 }.
% 0.70/1.11 (312) {G2,W3,D2,L1,V0,M1} R(304,53) { icext( uri_rdfs_Class, uri_rdf_Bag )
% 0.70/1.11 }.
% 0.70/1.11 (77) {G0,W14,D2,L3,V4,M1} I { ! iext( uri_rdfs_subPropertyOf, X, Y ), iext
% 0.70/1.11 ( Y, Z, T ), ! iext( X, Z, T ) }.
% 0.70/1.11 (314) {G2,W3,D2,L1,V0,M1} R(305,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (316) {G2,W3,D2,L1,V0,M1} R(306,53) { icext( uri_rdfs_Class, uri_rdfs_Seq )
% 0.70/1.11 }.
% 0.70/1.11 (375) {G1,W2,D2,L1,V0,M1} R(75,87) { ip( uri_ex_sameCliqueAs ) }.
% 0.70/1.11 (374) {G1,W2,D2,L1,V0,M1} R(75,18) { ip( uri_rdfs_isDefinedBy ) }.
% 0.70/1.11 (75) {G0,W7,D2,L2,V2,M1} I { ip( X ), ! iext( uri_rdfs_subPropertyOf, X, Y
% 0.70/1.11 ) }.
% 0.70/1.11 (323) {G5,W3,D2,L1,V0,M1} R(318,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (325) {G2,W3,D2,L1,V0,M1} R(319,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Container ) }.
% 0.70/1.11 (327) {G2,W3,D2,L1,V0,M1} R(320,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Literal ) }.
% 0.70/1.11 (329) {G2,W3,D2,L1,V0,M1} R(321,53) { icext( uri_rdfs_Class, uri_rdfs_Class
% 0.70/1.11 ) }.
% 0.70/1.11 (73) {G0,W14,D2,L3,V3,M1} I { ! iext( uri_rdfs_subClassOf, X, Z ), iext(
% 0.70/1.11 uri_rdfs_subClassOf, X, Y ), ! iext( uri_rdfs_subClassOf, Z, Y ) }.
% 0.70/1.11 (338) {G2,W3,D2,L1,V0,M1} R(322,53) { icext( uri_rdfs_Class, skol1 ) }.
% 0.70/1.11 (340) {G2,W3,D2,L1,V0,M1} R(307,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdf_XMLLiteral ) }.
% 0.70/1.11 (342) {G2,W3,D2,L1,V0,M1} R(308,53) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdfs_Datatype ) }.
% 0.70/1.11 (344) {G2,W3,D2,L1,V0,M1} R(309,53) { icext( uri_rdfs_Class, uri_ex_Clique
% 0.70/1.11 ) }.
% 0.70/1.11 (72) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X, X ), ! ic( X )
% 0.70/1.11 }.
% 0.70/1.11 (309) {G1,W2,D2,L1,V0,M1} R(68,89) { ic( uri_ex_Clique ) }.
% 0.70/1.11 (308) {G1,W2,D2,L1,V0,M1} R(68,49) { ic( uri_rdfs_Datatype ) }.
% 0.70/1.11 (307) {G1,W2,D2,L1,V0,M1} R(68,46) { ic( uri_rdf_XMLLiteral ) }.
% 0.70/1.11 (322) {G1,W2,D2,L1,V0,M1} R(69,89) { ic( skol1 ) }.
% 0.70/1.11 (70) {G0,W12,D2,L3,V3,M1} I { ! icext( X, Z ), icext( Y, Z ), ! iext(
% 0.70/1.11 uri_rdfs_subClassOf, X, Y ) }.
% 0.70/1.11 (321) {G1,W2,D2,L1,V0,M1} R(69,49) { ic( uri_rdfs_Class ) }.
% 0.70/1.11 (320) {G1,W2,D2,L1,V0,M1} R(69,46) { ic( uri_rdfs_Literal ) }.
% 0.70/1.11 (319) {G1,W2,D2,L1,V0,M1} R(69,30) { ic( uri_rdfs_Container ) }.
% 0.70/1.11 (318) {G4,W2,D2,L1,V0,M1} R(69,249) { ic( uri_rdfs_Resource ) }.
% 0.70/1.11 (69) {G0,W7,D2,L2,V2,M1} I { ic( Y ), ! iext( uri_rdfs_subClassOf, X, Y )
% 0.70/1.11 }.
% 0.70/1.11 (306) {G1,W2,D2,L1,V0,M1} R(68,45) { ic( uri_rdfs_Seq ) }.
% 0.70/1.11 (305) {G1,W2,D2,L1,V0,M1} R(68,33) { ic(
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (304) {G1,W2,D2,L1,V0,M1} R(68,31) { ic( uri_rdf_Bag ) }.
% 0.70/1.11 (303) {G1,W2,D2,L1,V0,M1} R(68,30) { ic( uri_rdf_Alt ) }.
% 0.70/1.11 (68) {G0,W7,D2,L2,V2,M1} I { ic( X ), ! iext( uri_rdfs_subClassOf, X, Y )
% 0.70/1.11 }.
% 0.70/1.11 (301) {G2,W4,D2,L1,V0,M1} R(257,12) { iext( uri_rdf_type, uri_owl_sameAs,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (257) {G1,W2,D2,L1,V0,M1} R(76,87) { ip( uri_owl_sameAs ) }.
% 0.70/1.11 (256) {G1,W2,D2,L1,V0,M1} R(76,18) { ip( uri_rdfs_seeAlso ) }.
% 0.70/1.11 (255) {G3,W2,D2,L1,V0,M1} R(76,165) { ip( uri_rdfs_member ) }.
% 0.70/1.11 (60) {G0,W13,D2,L3,V4,M1} I { icext( X, Y ), ! iext( uri_rdfs_range, Z, X )
% 0.70/1.11 , ! iext( Z, T, Y ) }.
% 0.70/1.11 (76) {G0,W7,D2,L2,V2,M1} I { ip( Y ), ! iext( uri_rdfs_subPropertyOf, X, Y
% 0.70/1.11 ) }.
% 0.70/1.11 (165) {G2,W4,D2,L1,V0,M1} R(32,133) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__1, uri_rdfs_member ) }.
% 0.70/1.11 (164) {G2,W4,D2,L1,V0,M1} R(32,134) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__2, uri_rdfs_member ) }.
% 0.70/1.11 (163) {G2,W4,D2,L1,V0,M1} R(32,135) { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf__3, uri_rdfs_member ) }.
% 0.70/1.11 (56) {G0,W6,D2,L2,V1,M1} I { icext( uri_rdfs_Literal, X ), ! lv( X ) }.
% 0.70/1.11 (249) {G3,W4,D2,L1,V0,M1} R(248,25) { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdf_Property, uri_rdfs_Resource ) }.
% 0.70/1.11 (162) {G2,W4,D2,L1,V1,M1} R(24,55) { iext( uri_rdf_type, X,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (161) {G1,W3,D2,L1,V0,M1} R(23,104) { icext( uri_ex_JoesGang, uri_ex_bob )
% 0.70/1.11 }.
% 0.70/1.11 (248) {G2,W2,D2,L1,V0,M1} R(54,137) { ic( uri_rdf_Property ) }.
% 0.70/1.11 (54) {G0,W6,D2,L2,V1,M1} I { ic( X ), ! icext( uri_rdfs_Class, X ) }.
% 0.70/1.11 (160) {G1,W3,D2,L1,V0,M1} R(23,103) { icext( uri_ex_JoesGang, uri_ex_alice
% 0.70/1.11 ) }.
% 0.70/1.11 (159) {G1,W3,D2,L1,V0,M1} R(23,102) { icext( uri_ex_Clique, uri_ex_JoesGang
% 0.70/1.11 ) }.
% 0.70/1.11 (158) {G1,W3,D2,L1,V0,M1} R(23,2) { icext( uri_rdf_Property, uri_rdf_first
% 0.70/1.11 ) }.
% 0.70/1.11 (157) {G1,W3,D2,L1,V0,M1} R(23,3) { icext( uri_rdf_List, uri_rdf_nil ) }.
% 0.70/1.11 (53) {G0,W6,D2,L2,V1,M1} I { icext( uri_rdfs_Class, X ), ! ic( X ) }.
% 0.70/1.11 (156) {G1,W3,D2,L1,V0,M1} R(23,4) { icext( uri_rdf_Property, uri_rdf_rest )
% 0.70/1.11 }.
% 0.70/1.11 (155) {G1,W3,D2,L1,V0,M1} R(23,93) { icext( uri_owl_ObjectProperty,
% 0.70/1.11 uri_foaf_knows ) }.
% 0.70/1.11 (154) {G1,W3,D2,L1,V0,M1} R(23,5) { icext( uri_rdf_Property, uri_rdf__1 )
% 0.70/1.11 }.
% 0.70/1.11 (153) {G1,W3,D2,L1,V0,M1} R(23,90) { icext( uri_owl_Restriction, skol1 )
% 0.70/1.11 }.
% 0.70/1.11 (51) {G0,W13,D2,L3,V4,M1} I { icext( X, Y ), ! iext( uri_rdfs_domain, Z, X
% 0.70/1.11 ), ! iext( Z, Y, T ) }.
% 0.70/1.11 (152) {G1,W3,D2,L1,V0,M1} R(23,6) { icext( uri_rdf_Property, uri_rdf__2 )
% 0.70/1.11 }.
% 0.70/1.11 (151) {G1,W3,D2,L1,V0,M1} R(23,7) { icext( uri_rdf_Property, uri_rdf__3 )
% 0.70/1.11 }.
% 0.70/1.11 (150) {G1,W3,D2,L1,V0,M1} R(23,86) { icext( uri_owl_Class, uri_ex_Clique )
% 0.70/1.11 }.
% 0.70/1.11 (149) {G1,W3,D2,L1,V0,M1} R(23,8) { icext( uri_rdf_Property, uri_rdf_object
% 0.70/1.11 ) }.
% 0.70/1.11 (48) {G0,W8,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X, uri_rdfs_Literal
% 0.70/1.11 ), ! icext( uri_rdfs_Datatype, X ) }.
% 0.70/1.11 (148) {G1,W3,D2,L1,V0,M1} R(23,9) { icext( uri_rdf_Property, uri_rdf_value
% 0.70/1.11 ) }.
% 0.70/1.11 (147) {G1,W3,D2,L1,V0,M1} R(23,10) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdf_subject ) }.
% 0.70/1.11 (146) {G3,W3,D2,L1,V0,M1} R(23,125) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_domain ) }.
% 0.70/1.11 (145) {G3,W3,D2,L1,V0,M1} R(23,126) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_subPropertyOf ) }.
% 0.70/1.11 (32) {G0,W8,D2,L2,V1,M1} I { iext( uri_rdfs_subPropertyOf, X,
% 0.70/1.11 uri_rdfs_member ), ! icext( uri_rdfs_ContainerMembershipProperty, X ) }.
% 0.70/1.11 (144) {G1,W3,D2,L1,V0,M1} R(23,13) { icext( uri_rdf_Property, uri_rdf_type
% 0.70/1.11 ) }.
% 0.70/1.11 (143) {G3,W3,D2,L1,V0,M1} R(23,127) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_range ) }.
% 0.70/1.11 (142) {G3,W3,D2,L1,V0,M1} R(23,128) { icext( uri_rdf_Property,
% 0.70/1.11 uri_rdfs_subClassOf ) }.
% 0.70/1.11 (141) {G3,W3,D2,L1,V0,M1} R(23,129) { icext( uri_rdf_Property,
% 0.70/1.11 uri_owl_onProperty ) }.
% 0.70/1.11 (25) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X,
% 0.70/1.11 uri_rdfs_Resource ), ! ic( X ) }.
% 0.70/1.11 (140) {G3,W3,D2,L1,V0,M1} R(23,130) { icext( uri_rdf_Property,
% 0.70/1.11 uri_owl_someValuesFrom ) }.
% 0.70/1.11 (139) {G3,W3,D2,L1,V0,M1} R(23,131) { icext( uri_rdf_Property,
% 0.70/1.11 uri_owl_propertyChainAxiom ) }.
% 0.70/1.11 (138) {G3,W3,D2,L1,V0,M1} R(23,132) { icext( uri_rdf_Property,
% 0.70/1.11 uri_owl_inverseOf ) }.
% 0.70/1.11 (137) {G1,W3,D2,L1,V0,M1} R(23,58) { icext( uri_rdfs_Class,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (24) {G0,W8,D2,L2,V2,M1} I { iext( uri_rdf_type, X, Y ), ! icext( Y, X )
% 0.70/1.11 }.
% 0.70/1.11 (136) {G1,W3,D2,L1,V0,M1} R(23,47) { icext( uri_rdfs_Datatype,
% 0.70/1.11 uri_rdf_XMLLiteral ) }.
% 0.70/1.11 (135) {G1,W3,D2,L1,V0,M1} R(23,44) { icext(
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdf__3 ) }.
% 0.70/1.11 (134) {G1,W3,D2,L1,V0,M1} R(23,43) { icext(
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdf__2 ) }.
% 0.70/1.11 (133) {G1,W3,D2,L1,V0,M1} R(23,42) { icext(
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdf__1 ) }.
% 0.70/1.11 (23) {G0,W8,D2,L2,V2,M1} I { icext( Y, X ), ! iext( uri_rdf_type, X, Y )
% 0.70/1.11 }.
% 0.70/1.11 (57) {G0,W6,D2,L2,V1,M1} I { lv( X ), ! icext( uri_rdfs_Literal, X ) }.
% 0.70/1.11 (85) {G0,W5,D2,L1,V0,M1} I { ! iext( uri_foaf_knows, uri_ex_alice,
% 0.70/1.11 uri_ex_bob ) }.
% 0.70/1.11 (22) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_seeAlso,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (26) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_first,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (21) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_seeAlso,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (27) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_first,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (28) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_rest,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (29) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_rest,
% 0.70/1.11 uri_rdf_List ) }.
% 0.70/1.11 (30) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_Alt,
% 0.70/1.11 uri_rdfs_Container ) }.
% 0.70/1.11 (20) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_label,
% 0.70/1.11 uri_rdfs_Literal ) }.
% 0.70/1.11 (31) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_Bag,
% 0.70/1.11 uri_rdfs_Container ) }.
% 0.70/1.11 (33) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty, uri_rdf_Property ) }.
% 0.70/1.11 (34) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_member,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (35) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_member,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (19) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_label,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (36) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__1,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (37) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__2,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (38) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__3,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (39) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__1,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (18) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdfs_isDefinedBy, uri_rdfs_seeAlso ) }.
% 0.70/1.11 (40) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__2,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (41) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__3,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (42) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__1,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (43) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__2,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (17) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_isDefinedBy,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (44) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__3,
% 0.70/1.11 uri_rdfs_ContainerMembershipProperty ) }.
% 0.70/1.11 (45) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdfs_Seq,
% 0.70/1.11 uri_rdfs_Container ) }.
% 0.70/1.11 (46) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_XMLLiteral
% 0.70/1.11 , uri_rdfs_Literal ) }.
% 0.70/1.11 (47) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_XMLLiteral,
% 0.70/1.11 uri_rdfs_Datatype ) }.
% 0.70/1.11 (16) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_isDefinedBy,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (49) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdfs_Datatype,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (50) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_domain,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (52) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_domain,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (58) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_Property,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (15) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_comment,
% 0.70/1.11 uri_rdfs_Literal ) }.
% 0.70/1.11 (59) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_range,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (61) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_range,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (132) {G2,W4,D2,L1,V0,M1} R(12,109) { iext( uri_rdf_type, uri_owl_inverseOf
% 0.70/1.11 , uri_rdf_Property ) }.
% 0.70/1.11 (131) {G2,W4,D2,L1,V0,M1} R(12,112) { iext( uri_rdf_type,
% 0.70/1.11 uri_owl_propertyChainAxiom, uri_rdf_Property ) }.
% 0.70/1.11 (14) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_comment,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (130) {G2,W4,D2,L1,V0,M1} R(12,113) { iext( uri_rdf_type,
% 0.70/1.11 uri_owl_someValuesFrom, uri_rdf_Property ) }.
% 0.70/1.11 (129) {G2,W4,D2,L1,V0,M1} R(12,114) { iext( uri_rdf_type,
% 0.70/1.11 uri_owl_onProperty, uri_rdf_Property ) }.
% 0.70/1.11 (128) {G2,W4,D2,L1,V0,M1} R(12,115) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_subClassOf, uri_rdf_Property ) }.
% 0.70/1.11 (127) {G2,W4,D2,L1,V0,M1} R(12,116) { iext( uri_rdf_type, uri_rdfs_range,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (13) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_type,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (126) {G2,W4,D2,L1,V0,M1} R(12,117) { iext( uri_rdf_type,
% 0.70/1.11 uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.70/1.11 (125) {G2,W4,D2,L1,V0,M1} R(12,118) { iext( uri_rdf_type, uri_rdfs_domain,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (124) {G1,W2,D2,L1,V0,M1} R(11,5) { ip( uri_rdf__1 ) }.
% 0.70/1.11 (123) {G1,W2,D2,L1,V0,M1} R(11,6) { ip( uri_rdf__2 ) }.
% 0.70/1.11 (12) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdf_type, X, uri_rdf_Property ), !
% 0.70/1.11 ip( X ) }.
% 0.70/1.11 (122) {G1,W2,D2,L1,V0,M1} R(11,7) { ip( uri_rdf__3 ) }.
% 0.70/1.11 (121) {G1,W2,D2,L1,V0,M1} R(11,8) { ip( uri_rdf_object ) }.
% 0.70/1.11 (120) {G1,W2,D2,L1,V0,M1} R(11,9) { ip( uri_rdf_value ) }.
% 0.70/1.11 (119) {G1,W2,D2,L1,V0,M1} R(11,10) { ip( uri_rdf_subject ) }.
% 0.70/1.11 (11) {G0,W7,D2,L2,V1,M1} I { ip( X ), ! iext( uri_rdf_type, X,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (62) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_object,
% 0.70/1.11 uri_rdfs_Statement ) }.
% 0.70/1.11 (63) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_predicate,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (64) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_predicate,
% 0.70/1.11 uri_rdfs_Statement ) }.
% 0.70/1.11 (65) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_subject,
% 0.70/1.11 uri_rdfs_Statement ) }.
% 0.70/1.11 (10) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_subject,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (66) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_subject,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (67) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (71) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_subClassOf,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (74) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_subPropertyOf
% 0.70/1.11 , uri_rdf_Property ) }.
% 0.70/1.11 (9) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_value,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (78) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (81) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_type,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (82) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_type,
% 0.70/1.11 uri_rdfs_Class ) }.
% 0.70/1.11 (118) {G1,W2,D2,L1,V0,M1} R(83,0) { ip( uri_rdfs_domain ) }.
% 0.70/1.11 (8) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_object,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (83) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_value,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (84) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_value,
% 0.70/1.11 uri_rdfs_Resource ) }.
% 0.70/1.11 (86) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_ex_Clique,
% 0.70/1.11 uri_owl_Class ) }.
% 0.70/1.11 (117) {G1,W2,D2,L1,V0,M1} R(87,0) { ip( uri_rdfs_subPropertyOf ) }.
% 0.70/1.11 (7) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__3,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (87) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subPropertyOf,
% 0.70/1.11 uri_ex_sameCliqueAs, uri_owl_sameAs ) }.
% 0.70/1.11 (116) {G1,W2,D2,L1,V0,M1} R(88,0) { ip( uri_rdfs_range ) }.
% 0.70/1.11 (88) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_ex_sameCliqueAs,
% 0.70/1.11 uri_ex_Clique ) }.
% 0.70/1.11 (115) {G1,W2,D2,L1,V0,M1} R(89,0) { ip( uri_rdfs_subClassOf ) }.
% 0.70/1.11 (6) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__2,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (89) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_ex_Clique,
% 0.70/1.11 skol1 ) }.
% 0.70/1.11 (90) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, skol1, uri_owl_Restriction
% 0.70/1.11 ) }.
% 0.70/1.11 (114) {G1,W2,D2,L1,V0,M1} R(91,0) { ip( uri_owl_onProperty ) }.
% 0.70/1.11 (91) {G0,W4,D2,L1,V0,M1} I { iext( uri_owl_onProperty, skol1,
% 0.70/1.11 uri_ex_sameCliqueAs ) }.
% 0.70/1.11 (5) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__1,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (113) {G1,W2,D2,L1,V0,M1} R(92,0) { ip( uri_owl_someValuesFrom ) }.
% 0.70/1.11 (92) {G0,W4,D2,L1,V0,M1} I { iext( uri_owl_someValuesFrom, skol1,
% 0.70/1.11 uri_ex_Clique ) }.
% 0.70/1.11 (93) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_foaf_knows,
% 0.70/1.11 uri_owl_ObjectProperty ) }.
% 0.70/1.11 (112) {G1,W2,D2,L1,V0,M1} R(94,0) { ip( uri_owl_propertyChainAxiom ) }.
% 0.70/1.11 (4) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_rest,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (94) {G0,W4,D2,L1,V0,M1} I { iext( uri_owl_propertyChainAxiom,
% 0.70/1.11 uri_foaf_knows, skol2 ) }.
% 0.70/1.11 (95) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_first, skol2, uri_rdf_type ) }.
% 0.70/1.11 (96) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_rest, skol2, skol3 ) }.
% 0.70/1.11 (97) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_first, skol3,
% 0.70/1.11 uri_ex_sameCliqueAs ) }.
% 0.70/1.11 (3) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_nil, uri_rdf_List )
% 0.70/1.11 }.
% 0.70/1.11 (98) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_rest, skol3, skol4 ) }.
% 0.70/1.11 (111) {G1,W2,D2,L1,V0,M1} R(99,0) { ip( uri_rdf_first ) }.
% 0.70/1.11 (99) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_first, skol4, skol5 ) }.
% 0.70/1.11 (110) {G1,W2,D2,L1,V0,M1} R(100,0) { ip( uri_rdf_rest ) }.
% 0.70/1.11 (2) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_first,
% 0.70/1.11 uri_rdf_Property ) }.
% 0.70/1.11 (100) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_rest, skol4, uri_rdf_nil ) }.
% 0.70/1.11 (109) {G1,W2,D2,L1,V0,M1} R(101,0) { ip( uri_owl_inverseOf ) }.
% 0.70/1.11 (101) {G0,W4,D2,L1,V0,M1} I { iext( uri_owl_inverseOf, skol5, uri_rdf_type
% 0.70/1.11 ) }.
% 0.70/1.11 (108) {G1,W2,D2,L1,V0,M1} R(0,102) { ip( uri_rdf_type ) }.
% 0.70/1.11 (0) {G0,W7,D2,L2,V3,M1} I { ip( X ), ! iext( X, Y, Z ) }.
% 0.70/1.11 (102) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_ex_JoesGang,
% 0.70/1.11 uri_ex_Clique ) }.
% 0.70/1.11 (103) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_ex_alice,
% 0.70/1.11 uri_ex_JoesGang ) }.
% 0.70/1.11 (104) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_ex_bob,
% 0.70/1.11 uri_ex_JoesGang ) }.
% 0.70/1.11 (55) {G1,W3,D2,L1,V1,M1} I;r(1) { icext( uri_rdfs_Resource, X ) }.
% 0.70/1.11 (1) {G0,W2,D2,L1,V1,M1} I { ir( X ) }.
% 0.70/1.11
% 0.70/1.11
% 0.70/1.11 % SZS output end Saturation
% 0.70/1.11 end of saturation!
% 0.70/1.11
% 0.70/1.11 Memory use:
% 0.70/1.11
% 0.70/1.11 space for terms: 6156
% 0.70/1.11 space for clauses: 33739
% 0.70/1.11
% 0.70/1.11
% 0.70/1.11 clauses generated: 1771
% 0.70/1.11 clauses kept: 729
% 0.70/1.11 clauses selected: 703
% 0.70/1.11 clauses deleted: 26
% 0.70/1.11 clauses inuse deleted: 0
% 0.70/1.11
% 0.70/1.11 subsentry: 2547
% 0.70/1.11 literals s-matched: 1062
% 0.70/1.11 literals matched: 1028
% 0.70/1.11 full subsumption: 6
% 0.70/1.11
% 0.70/1.11 checksum: -169467419
% 0.70/1.11
% 0.70/1.11
% 0.70/1.11 Bliksem ended
%------------------------------------------------------------------------------