↑ Up

Bliksem---1.12.CSA-Sat.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Bliksem---1.12
% Problem  : SWB005+4 : TPTP v8.1.0. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : bliksem %s

% Computer : n025.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:29 EDT 2022

% Result   : CounterSatisfiable 0.72s 1.09s
% Output   : Saturation 0.72s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : SWB005+4 : TPTP v8.1.0. Released v5.2.0.
% 0.06/0.12  % Command  : bliksem %s
% 0.12/0.33  % Computer : n025.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 06:14:58 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.72/1.08  *** allocated 10000 integers for termspace/termends
% 0.72/1.08  *** allocated 10000 integers for clauses
% 0.72/1.08  *** allocated 10000 integers for justifications
% 0.72/1.08  Bliksem 1.12
% 0.72/1.08  
% 0.72/1.08  
% 0.72/1.08  Automatic Strategy Selection
% 0.72/1.08  
% 0.72/1.08  
% 0.72/1.08  Clauses:
% 0.72/1.08  
% 0.72/1.08  { ! iext( X, Y, Z ), ip( X ) }.
% 0.72/1.08  { ir( X ) }.
% 0.72/1.08  { ! lv( X ), ir( X ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_first, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_nil, uri_rdf_List ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_rest, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__1, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__2, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__3, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_object, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_value, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_subject, uri_rdf_Property ) }.
% 0.72/1.08  { ! iext( uri_rdf_type, X, uri_rdf_Property ), ip( X ) }.
% 0.72/1.08  { ! ip( X ), iext( uri_rdf_type, X, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_type, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_type, uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso ) }
% 0.72/1.08    .
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource ) }.
% 0.72/1.08  { ! iext( uri_rdf_type, X, Y ), icext( Y, X ) }.
% 0.72/1.08  { ! icext( Y, X ), iext( uri_rdf_type, X, Y ) }.
% 0.72/1.08  { ! ic( X ), iext( uri_rdfs_subClassOf, X, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdf_first, uri_rdf_List ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdf_rest, uri_rdf_List ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdf_rest, uri_rdf_List ) }.
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container ) }.
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container ) }.
% 0.72/1.08  { ! icext( uri_rdfs_ContainerMembershipProperty, X ), iext( 
% 0.72/1.08    uri_rdfs_subPropertyOf, X, uri_rdfs_member ) }.
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, 
% 0.72/1.08    uri_rdf_Property ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty ) }
% 0.72/1.08    .
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty ) }
% 0.72/1.08    .
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty ) }
% 0.72/1.08    .
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container ) }.
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype ) }.
% 0.72/1.08  { ! icext( uri_rdfs_Datatype, X ), iext( uri_rdfs_subClassOf, X, 
% 0.72/1.08    uri_rdfs_Literal ) }.
% 0.72/1.08  { iext( uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property ) }.
% 0.72/1.08  { ! iext( uri_rdfs_domain, Z, X ), ! iext( Z, Y, T ), icext( X, Y ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class ) }.
% 0.72/1.08  { ! ic( X ), icext( uri_rdfs_Class, X ) }.
% 0.72/1.08  { ! icext( uri_rdfs_Class, X ), ic( X ) }.
% 0.72/1.08  { ! ir( X ), icext( uri_rdfs_Resource, X ) }.
% 0.72/1.08  { ! icext( uri_rdfs_Resource, X ), ir( X ) }.
% 0.72/1.08  { ! lv( X ), icext( uri_rdfs_Literal, X ) }.
% 0.72/1.08  { ! icext( uri_rdfs_Literal, X ), lv( X ) }.
% 0.72/1.08  { iext( uri_rdf_type, uri_rdf_Property, uri_rdfs_Class ) }.
% 0.72/1.08  { iext( uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property ) }.
% 0.72/1.08  { ! iext( uri_rdfs_range, Z, X ), ! iext( Z, T, Y ), icext( X, Y ) }.
% 0.72/1.08  { iext( uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subClassOf, X, Y ), ic( X ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subClassOf, X, Y ), ic( Y ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subClassOf, X, Y ), ! icext( X, Z ), icext( Y, Z ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class ) }.
% 0.72/1.09  { ! ic( X ), iext( uri_rdfs_subClassOf, X, X ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subClassOf, X, Z ), ! iext( uri_rdfs_subClassOf, Z, Y )
% 0.72/1.09    , iext( uri_rdfs_subClassOf, X, Y ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subPropertyOf, X, Y ), ip( X ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subPropertyOf, X, Y ), ip( Y ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subPropertyOf, X, Y ), ! iext( X, Z, T ), iext( Y, Z, T
% 0.72/1.09     ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.72/1.09  { ! ip( X ), iext( uri_rdfs_subPropertyOf, X, X ) }.
% 0.72/1.09  { ! iext( uri_rdfs_subPropertyOf, X, Z ), ! iext( uri_rdfs_subPropertyOf, Z
% 0.72/1.09    , Y ), iext( uri_rdfs_subPropertyOf, X, Y ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdf_type, uri_rdfs_Class ) }.
% 0.72/1.09  { iext( uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource ) }.
% 0.72/1.09  { iext( uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource ) }.
% 0.72/1.09  { ! iext( uri_rdf_type, uri_ex_s, uri_rdfs_Resource ), ! iext( uri_rdf_type
% 0.72/1.09    , uri_ex_s, uri_owl_Thing ), ! iext( uri_rdf_type, uri_ex_p, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdf_type, uri_ex_p, uri_owl_Thing ), ! 
% 0.72/1.09    iext( uri_rdf_type, uri_ex_p, uri_rdf_Property ), ! iext( uri_rdf_type, 
% 0.72/1.09    uri_ex_p, uri_owl_ObjectProperty ), ! iext( uri_rdf_type, uri_ex_o, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdf_type, uri_ex_o, uri_owl_Thing ) }.
% 0.72/1.09  { iext( uri_ex_p, uri_ex_s, uri_ex_o ) }.
% 0.72/1.09  
% 0.72/1.09  percentage equality = 0.000000, percentage horn = 1.000000
% 0.72/1.09  This is a near-Horn, non-equality  problem
% 0.72/1.09  
% 0.72/1.09  
% 0.72/1.09  Options Used:
% 0.72/1.09  
% 0.72/1.09  useres =            1
% 0.72/1.09  useparamod =        0
% 0.72/1.09  useeqrefl =         0
% 0.72/1.09  useeqfact =         0
% 0.72/1.09  usefactor =         1
% 0.72/1.09  usesimpsplitting =  0
% 0.72/1.09  usesimpdemod =      0
% 0.72/1.09  usesimpres =        4
% 0.72/1.09  
% 0.72/1.09  resimpinuse      =  1000
% 0.72/1.09  resimpclauses =     20000
% 0.72/1.09  substype =          standard
% 0.72/1.09  backwardsubs =      1
% 0.72/1.09  selectoldest =      5
% 0.72/1.09  
% 0.72/1.09  litorderings [0] =  split
% 0.72/1.09  litorderings [1] =  liftord
% 0.72/1.09  
% 0.72/1.09  termordering =      none
% 0.72/1.09  
% 0.72/1.09  litapriori =        1
% 0.72/1.09  termapriori =       0
% 0.72/1.09  litaposteriori =    0
% 0.72/1.09  termaposteriori =   0
% 0.72/1.09  demodaposteriori =  0
% 0.72/1.09  ordereqreflfact =   0
% 0.72/1.09  
% 0.72/1.09  litselect =         negative
% 0.72/1.09  
% 0.72/1.09  maxweight =         30000
% 0.72/1.09  maxdepth =          30000
% 0.72/1.09  maxlength =         115
% 0.72/1.09  maxnrvars =         195
% 0.72/1.09  excuselevel =       0
% 0.72/1.09  increasemaxweight = 0
% 0.72/1.09  
% 0.72/1.09  maxselected =       10000000
% 0.72/1.09  maxnrclauses =      10000000
% 0.72/1.09  
% 0.72/1.09  showgenerated =    0
% 0.72/1.09  showkept =         0
% 0.72/1.09  showselected =     0
% 0.72/1.09  showdeleted =      0
% 0.72/1.09  showresimp =       1
% 0.72/1.09  showstatus =       2000
% 0.72/1.09  
% 0.72/1.09  prologoutput =     0
% 0.72/1.09  nrgoals =          5000000
% 0.72/1.09  totalproof =       1
% 0.72/1.09  
% 0.72/1.09  Symbols occurring in the translation:
% 0.72/1.09  
% 0.72/1.09  {}  [0, 0]      (w:1, o:2, a:1, s:1, b:0), 
% 0.72/1.09  .  [1, 2]      (w:1, o:63, a:1, s:1, b:0), 
% 0.72/1.09  !  [4, 1]      (w:1, o:54, a:1, s:1, b:0), 
% 0.72/1.09  =  [13, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.72/1.09  ==>  [14, 2]      (w:1, o:0, a:0, s:1, b:0), 
% 0.72/1.09  iext  [38, 3]      (w:1, o:88, a:1, s:1, b:0), 
% 0.72/1.09  ip  [39, 1]      (w:1, o:59, a:1, s:1, b:0), 
% 0.72/1.09  ir  [41, 1]      (w:1, o:60, a:1, s:1, b:0), 
% 0.72/1.09  lv  [42, 1]      (w:1, o:61, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_type  [43, 0]      (w:1, o:12, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_first  [44, 0]      (w:1, o:13, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_Property  [45, 0]      (w:1, o:14, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_nil  [46, 0]      (w:1, o:15, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_List  [47, 0]      (w:1, o:16, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_rest  [48, 0]      (w:1, o:17, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf__1  [49, 0]      (w:1, o:18, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf__2  [50, 0]      (w:1, o:19, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf__3  [51, 0]      (w:1, o:20, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_object  [52, 0]      (w:1, o:21, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_value  [53, 0]      (w:1, o:22, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_subject  [54, 0]      (w:1, o:11, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_domain  [55, 0]      (w:1, o:24, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_comment  [56, 0]      (w:1, o:23, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Resource  [57, 0]      (w:1, o:25, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_range  [58, 0]      (w:1, o:26, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Literal  [59, 0]      (w:1, o:27, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_isDefinedBy  [60, 0]      (w:1, o:28, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_subPropertyOf  [61, 0]      (w:1, o:29, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_seeAlso  [62, 0]      (w:1, o:30, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_label  [63, 0]      (w:1, o:31, a:1, s:1, b:0), 
% 0.72/1.09  icext  [65, 2]      (w:1, o:87, a:1, s:1, b:0), 
% 0.72/1.09  ic  [66, 1]      (w:1, o:62, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_subClassOf  [67, 0]      (w:1, o:33, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_Alt  [68, 0]      (w:1, o:34, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Container  [69, 0]      (w:1, o:35, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_Bag  [70, 0]      (w:1, o:36, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_ContainerMembershipProperty  [71, 0]      (w:1, o:37, a:1, s:1, b:
% 0.72/1.09    0), 
% 0.72/1.09  uri_rdfs_member  [72, 0]      (w:1, o:38, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Seq  [73, 0]      (w:1, o:39, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_XMLLiteral  [74, 0]      (w:1, o:40, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Datatype  [75, 0]      (w:1, o:42, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Class  [77, 0]      (w:1, o:41, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdfs_Statement  [79, 0]      (w:1, o:45, a:1, s:1, b:0), 
% 0.72/1.09  uri_rdf_predicate  [80, 0]      (w:1, o:46, a:1, s:1, b:0), 
% 0.72/1.09  uri_ex_s  [84, 0]      (w:1, o:49, a:1, s:1, b:0), 
% 0.72/1.09  uri_owl_Thing  [85, 0]      (w:1, o:50, a:1, s:1, b:0), 
% 0.72/1.09  uri_ex_p  [86, 0]      (w:1, o:52, a:1, s:1, b:0), 
% 0.72/1.09  uri_owl_ObjectProperty  [87, 0]      (w:1, o:53, a:1, s:1, b:0), 
% 0.72/1.09  uri_ex_o  [88, 0]      (w:1, o:51, a:1, s:1, b:0).
% 0.72/1.09  
% 0.72/1.09  
% 0.72/1.09  Starting Search:
% 0.72/1.09  
% 0.72/1.09  *** allocated 15000 integers for clauses
% 0.72/1.09  *** allocated 22500 integers for clauses
% 0.72/1.09  *** allocated 33750 integers for clauses
% 0.72/1.09  Resimplifying inuse:
% 0.72/1.09  Done
% 0.72/1.09  
% 0.72/1.09  
% 0.72/1.09  
% 0.72/1.09  found a saturation!
% 0.72/1.09  % SZS status CounterSatisfiable
% 0.72/1.09  % SZS output start Saturation
% 0.72/1.09  
% 0.72/1.09  (412) {G3,W20,D2,L4,V0,M1} S(85);r(129);r(104);r(129);r(129) { ! iext( 
% 0.72/1.09    uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty ), ! iext( uri_rdf_type, 
% 0.72/1.09    uri_ex_p, uri_owl_Thing ), ! iext( uri_rdf_type, uri_ex_o, uri_owl_Thing
% 0.72/1.09     ), ! iext( uri_rdf_type, uri_ex_s, uri_owl_Thing ) }.
% 0.72/1.09  (367) {G1,W9,D2,L2,V1,M1} R(77,86) { iext( X, uri_ex_s, uri_ex_o ), ! iext
% 0.72/1.09    ( uri_rdfs_subPropertyOf, uri_ex_p, X ) }.
% 0.72/1.09  (366) {G1,W9,D2,L2,V1,M1} R(77,84) { iext( X, uri_rdf_value, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (365) {G1,W9,D2,L2,V1,M1} R(77,83) { iext( X, uri_rdf_value, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (364) {G1,W9,D2,L2,V1,M1} R(77,82) { iext( X, uri_rdf_type, uri_rdfs_Class
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (363) {G1,W9,D2,L2,V1,M1} R(77,2) { iext( X, uri_rdf_first, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (362) {G1,W9,D2,L2,V1,M1} R(77,81) { iext( X, uri_rdf_type, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (361) {G1,W9,D2,L2,V1,M1} R(77,78) { iext( X, uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (360) {G1,W9,D2,L2,V1,M1} R(77,74) { iext( X, uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (359) {G1,W9,D2,L2,V1,M1} R(77,3) { iext( X, uri_rdf_nil, uri_rdf_List ), !
% 0.72/1.09     iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (358) {G1,W9,D2,L2,V1,M1} R(77,71) { iext( X, uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (357) {G1,W9,D2,L2,V1,M1} R(77,67) { iext( X, uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (356) {G1,W9,D2,L2,V1,M1} R(77,66) { iext( X, uri_rdf_subject, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (355) {G1,W9,D2,L2,V1,M1} R(77,65) { iext( X, uri_rdf_subject, 
% 0.72/1.09    uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.72/1.09     ) }.
% 0.72/1.09  (354) {G1,W9,D2,L2,V1,M1} R(77,4) { iext( X, uri_rdf_rest, uri_rdf_Property
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (353) {G1,W9,D2,L2,V1,M1} R(77,64) { iext( X, uri_rdf_predicate, 
% 0.72/1.09    uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.72/1.09     ) }.
% 0.72/1.09  (352) {G1,W9,D2,L2,V1,M1} R(77,63) { iext( X, uri_rdf_predicate, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (351) {G1,W9,D2,L2,V1,M1} R(77,62) { iext( X, uri_rdf_object, 
% 0.72/1.09    uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X
% 0.72/1.09     ) }.
% 0.72/1.09  (350) {G1,W9,D2,L2,V1,M1} R(77,61) { iext( X, uri_rdfs_range, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (349) {G1,W9,D2,L2,V1,M1} R(77,5) { iext( X, uri_rdf__1, uri_rdf_Property )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (348) {G1,W9,D2,L2,V1,M1} R(77,59) { iext( X, uri_rdfs_range, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (347) {G1,W9,D2,L2,V1,M1} R(77,58) { iext( X, uri_rdf_Property, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (346) {G1,W9,D2,L2,V1,M1} R(77,52) { iext( X, uri_rdfs_domain, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (345) {G1,W9,D2,L2,V1,M1} R(77,50) { iext( X, uri_rdfs_domain, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (344) {G1,W9,D2,L2,V1,M1} R(77,6) { iext( X, uri_rdf__2, uri_rdf_Property )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (343) {G1,W9,D2,L2,V1,M1} R(77,49) { iext( X, uri_rdfs_Datatype, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X
% 0.72/1.09     ) }.
% 0.72/1.09  (342) {G1,W9,D2,L2,V1,M1} R(77,47) { iext( X, uri_rdf_XMLLiteral, 
% 0.72/1.09    uri_rdfs_Datatype ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X )
% 0.72/1.09     }.
% 0.72/1.09  (341) {G1,W9,D2,L2,V1,M1} R(77,46) { iext( X, uri_rdf_XMLLiteral, 
% 0.72/1.09    uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, 
% 0.72/1.09    X ) }.
% 0.72/1.09  (340) {G1,W9,D2,L2,V1,M1} R(77,7) { iext( X, uri_rdf__3, uri_rdf_Property )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (339) {G1,W9,D2,L2,V1,M1} R(77,45) { iext( X, uri_rdfs_Seq, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (338) {G1,W9,D2,L2,V1,M1} R(77,44) { iext( X, uri_rdf__3, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_type, X ) }.
% 0.72/1.09  (337) {G1,W9,D2,L2,V1,M1} R(77,43) { iext( X, uri_rdf__2, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_type, X ) }.
% 0.72/1.09  (336) {G1,W9,D2,L2,V1,M1} R(77,42) { iext( X, uri_rdf__1, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_type, X ) }.
% 0.72/1.09  (335) {G1,W9,D2,L2,V1,M1} R(77,8) { iext( X, uri_rdf_object, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (334) {G1,W9,D2,L2,V1,M1} R(77,41) { iext( X, uri_rdf__3, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (333) {G1,W9,D2,L2,V1,M1} R(77,40) { iext( X, uri_rdf__2, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (332) {G1,W9,D2,L2,V1,M1} R(77,39) { iext( X, uri_rdf__1, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (331) {G1,W9,D2,L2,V1,M1} R(77,38) { iext( X, uri_rdf__3, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.72/1.09  (330) {G1,W9,D2,L2,V1,M1} R(77,9) { iext( X, uri_rdf_value, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (329) {G1,W9,D2,L2,V1,M1} R(77,37) { iext( X, uri_rdf__2, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.72/1.09  (328) {G1,W9,D2,L2,V1,M1} R(77,36) { iext( X, uri_rdf__1, uri_rdfs_Resource
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.72/1.09  (327) {G1,W9,D2,L2,V1,M1} R(77,35) { iext( X, uri_rdfs_member, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (326) {G1,W9,D2,L2,V1,M1} R(77,34) { iext( X, uri_rdfs_member, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (325) {G1,W9,D2,L2,V1,M1} R(77,10) { iext( X, uri_rdf_subject, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (324) {G1,W9,D2,L2,V1,M1} R(77,33) { iext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty, uri_rdf_Property ), ! iext( 
% 0.72/1.09    uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (323) {G1,W9,D2,L2,V1,M1} R(77,31) { iext( X, uri_rdf_Bag, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (322) {G1,W9,D2,L2,V1,M1} R(77,30) { iext( X, uri_rdf_Alt, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (321) {G1,W9,D2,L2,V1,M1} R(77,29) { iext( X, uri_rdf_rest, uri_rdf_List )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X ) }.
% 0.72/1.09  (320) {G1,W9,D2,L2,V1,M1} R(77,13) { iext( X, uri_rdf_type, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (319) {G3,W9,D2,L2,V1,M1} R(77,103) { iext( X, uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (318) {G3,W9,D2,L2,V1,M1} R(77,104) { iext( X, uri_ex_p, uri_rdf_Property )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (317) {G3,W9,D2,L2,V1,M1} R(77,105) { iext( X, uri_rdfs_range, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (316) {G3,W9,D2,L2,V1,M1} R(77,106) { iext( X, uri_rdfs_domain, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (315) {G1,W9,D2,L2,V1,M1} R(77,14) { iext( X, uri_rdfs_comment, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (314) {G1,W9,D2,L2,V1,M1} R(77,28) { iext( X, uri_rdf_rest, uri_rdf_List )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.72/1.09  (313) {G1,W9,D2,L2,V1,M1} R(77,27) { iext( X, uri_rdf_first, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (312) {G1,W9,D2,L2,V1,M1} R(77,26) { iext( X, uri_rdf_first, uri_rdf_List )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X ) }.
% 0.72/1.09  (311) {G1,W9,D2,L2,V1,M1} R(77,22) { iext( X, uri_rdfs_seeAlso, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (310) {G1,W9,D2,L2,V1,M1} R(77,15) { iext( X, uri_rdfs_comment, 
% 0.72/1.09    uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (309) {G1,W9,D2,L2,V1,M1} R(77,21) { iext( X, uri_rdfs_seeAlso, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (368) {G4,W9,D2,L2,V1,M1} R(292,77) { iext( X, uri_rdf_Alt, uri_rdfs_Class
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (308) {G1,W9,D2,L2,V1,M1} R(77,20) { iext( X, uri_rdfs_label, 
% 0.72/1.09    uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (369) {G4,W9,D2,L2,V1,M1} R(291,77) { iext( X, uri_rdf_Bag, uri_rdfs_Class
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (370) {G4,W9,D2,L2,V1,M1} R(290,77) { iext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class ), ! iext( 
% 0.72/1.09    uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (371) {G4,W9,D2,L2,V1,M1} R(289,77) { iext( X, uri_rdfs_Seq, uri_rdfs_Class
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (389) {G3,W9,D2,L2,V1,M1} R(372,77) { iext( X, uri_rdfs_isDefinedBy, 
% 0.72/1.09    uri_rdfs_isDefinedBy ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (307) {G1,W9,D2,L2,V1,M1} R(77,19) { iext( X, uri_rdfs_label, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (391) {G3,W9,D2,L2,V1,M1} R(373,77) { iext( X, uri_rdfs_seeAlso, 
% 0.72/1.09    uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (393) {G5,W9,D2,L2,V1,M1} R(374,77) { iext( X, uri_rdfs_member, 
% 0.72/1.09    uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (395) {G3,W9,D2,L2,V1,M1} R(375,77) { iext( X, uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (401) {G1,W9,D2,L2,V1,M1} R(80,18) { iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.09    uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.09    uri_rdfs_isDefinedBy ) }.
% 0.72/1.09  (306) {G1,W9,D2,L2,V1,M1} R(77,18) { iext( X, uri_rdfs_isDefinedBy, 
% 0.72/1.09    uri_rdfs_seeAlso ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (400) {G3,W9,D2,L2,V1,M1} R(80,130) { iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.09    uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__3 ) }.
% 0.72/1.09  (399) {G3,W9,D2,L2,V1,M1} R(80,131) { iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.09    uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__2 ) }.
% 0.72/1.09  (398) {G3,W9,D2,L2,V1,M1} R(80,132) { iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.09    uri_rdfs_member ), ! iext( uri_rdfs_subPropertyOf, X, uri_rdf__1 ) }.
% 0.72/1.09  (402) {G3,W9,D2,L2,V1,M1} R(376,77) { iext( X, uri_rdf_first, uri_rdf_first
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (305) {G1,W9,D2,L2,V1,M1} R(77,16) { iext( X, uri_rdfs_isDefinedBy, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_domain, X )
% 0.72/1.09     }.
% 0.72/1.09  (405) {G3,W9,D2,L2,V1,M1} R(377,77) { iext( X, uri_rdf_rest, uri_rdf_rest )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (408) {G3,W9,D2,L2,V1,M1} R(378,77) { iext( X, uri_rdf__1, uri_rdf__1 ), ! 
% 0.72/1.09    iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (410) {G3,W9,D2,L2,V1,M1} R(379,77) { iext( X, uri_rdf__2, uri_rdf__2 ), ! 
% 0.72/1.09    iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (413) {G3,W9,D2,L2,V1,M1} R(380,77) { iext( X, uri_rdf__3, uri_rdf__3 ), ! 
% 0.72/1.09    iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (304) {G3,W9,D2,L2,V1,M1} R(77,108) { iext( X, uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (415) {G3,W9,D2,L2,V1,M1} R(381,77) { iext( X, uri_rdf_object, 
% 0.72/1.09    uri_rdf_object ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (418) {G3,W9,D2,L2,V1,M1} R(382,77) { iext( X, uri_rdf_value, uri_rdf_value
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (421) {G3,W9,D2,L2,V1,M1} R(383,77) { iext( X, uri_rdf_subject, 
% 0.72/1.09    uri_rdf_subject ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (424) {G3,W9,D2,L2,V1,M1} R(384,77) { iext( X, uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdfs_subClassOf ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (303) {G1,W9,D2,L2,V1,M1} R(77,17) { iext( X, uri_rdfs_isDefinedBy, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_range, X )
% 0.72/1.09     }.
% 0.72/1.09  (427) {G3,W9,D2,L2,V1,M1} R(385,77) { iext( X, uri_rdf_type, uri_rdf_type )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (430) {G3,W9,D2,L2,V1,M1} R(386,77) { iext( X, uri_ex_p, uri_ex_p ), ! iext
% 0.72/1.09    ( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (433) {G3,W9,D2,L2,V1,M1} R(387,77) { iext( X, uri_rdfs_range, 
% 0.72/1.09    uri_rdfs_range ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (436) {G3,W9,D2,L2,V1,M1} R(388,77) { iext( X, uri_rdfs_domain, 
% 0.72/1.09    uri_rdfs_domain ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (301) {G3,W9,D2,L2,V1,M1} R(77,130) { iext( X, uri_rdf__3, uri_rdfs_member
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (439) {G7,W9,D2,L2,V1,M1} R(281,77) { iext( X, uri_rdfs_Resource, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (440) {G4,W9,D2,L2,V1,M1} R(280,77) { iext( X, uri_rdfs_Container, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (441) {G4,W9,D2,L2,V1,M1} R(279,77) { iext( X, uri_rdfs_Literal, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (442) {G4,W9,D2,L2,V1,M1} R(278,77) { iext( X, uri_rdfs_Class, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (300) {G3,W9,D2,L2,V1,M1} R(77,131) { iext( X, uri_rdf__2, uri_rdfs_member
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (443) {G3,W9,D2,L2,V1,M1} R(268,77) { iext( X, uri_rdfs_Datatype, 
% 0.72/1.09    uri_rdfs_Datatype ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (445) {G3,W9,D2,L2,V1,M1} R(269,77) { iext( X, uri_rdf_XMLLiteral, 
% 0.72/1.09    uri_rdf_XMLLiteral ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (447) {G3,W9,D2,L2,V1,M1} R(270,77) { iext( X, uri_rdfs_Class, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X
% 0.72/1.09     ) }.
% 0.72/1.09  (449) {G3,W9,D2,L2,V1,M1} R(271,77) { iext( X, uri_rdfs_Literal, 
% 0.72/1.09    uri_rdfs_Literal ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, 
% 0.72/1.09    X ) }.
% 0.72/1.09  (299) {G3,W9,D2,L2,V1,M1} R(77,132) { iext( X, uri_rdf__1, uri_rdfs_member
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (451) {G3,W9,D2,L2,V1,M1} R(272,77) { iext( X, uri_rdfs_Container, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (453) {G3,W9,D2,L2,V1,M1} R(273,77) { iext( X, uri_rdfs_Seq, uri_rdfs_Seq )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (455) {G3,W9,D2,L2,V1,M1} R(274,77) { iext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (457) {G3,W9,D2,L2,V1,M1} R(275,77) { iext( X, uri_rdf_Bag, uri_rdf_Bag ), 
% 0.72/1.09    ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (298) {G4,W9,D2,L2,V1,M1} R(77,199) { iext( X, uri_rdf_Property, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (459) {G3,W9,D2,L2,V1,M1} R(276,77) { iext( X, uri_rdf_Alt, uri_rdf_Alt ), 
% 0.72/1.09    ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (461) {G4,W9,D2,L2,V1,M1} R(277,77) { iext( X, uri_rdf_Property, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, 
% 0.72/1.09    X ) }.
% 0.72/1.09  (462) {G4,W9,D2,L2,V1,M1} R(267,77) { iext( X, uri_rdf_XMLLiteral, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (463) {G4,W9,D2,L2,V1,M1} R(266,77) { iext( X, uri_rdfs_Datatype, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (297) {G3,W9,D2,L2,V1,M1} R(77,228) { iext( X, uri_rdfs_seeAlso, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (465) {G3,W9,D2,L2,V1,M1} R(265,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Datatype )
% 0.72/1.09     }.
% 0.72/1.09  (464) {G3,W9,D2,L2,V1,M1} R(265,77) { iext( X, uri_rdfs_Datatype, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (467) {G3,W9,D2,L2,V1,M1} R(263,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral )
% 0.72/1.09     }.
% 0.72/1.09  (466) {G3,W9,D2,L2,V1,M1} R(263,77) { iext( X, uri_rdf_XMLLiteral, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (296) {G3,W9,D2,L2,V1,M1} R(77,294) { iext( X, uri_rdfs_isDefinedBy, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (469) {G3,W9,D2,L2,V1,M1} R(255,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Class ) }.
% 0.72/1.09  (468) {G3,W9,D2,L2,V1,M1} R(255,77) { iext( X, uri_rdfs_Class, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (471) {G3,W9,D2,L2,V1,M1} R(253,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Literal )
% 0.72/1.09     }.
% 0.72/1.09  (470) {G3,W9,D2,L2,V1,M1} R(253,77) { iext( X, uri_rdfs_Literal, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (288) {G1,W9,D2,L2,V1,M1} R(73,49) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Datatype ) }.
% 0.72/1.09  (473) {G3,W9,D2,L2,V1,M1} R(251,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Container )
% 0.72/1.09     }.
% 0.72/1.09  (472) {G3,W9,D2,L2,V1,M1} R(251,77) { iext( X, uri_rdfs_Container, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (474) {G6,W9,D2,L2,V1,M1} R(249,77) { iext( X, uri_rdfs_Resource, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (477) {G3,W9,D2,L2,V1,M1} R(243,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Seq ) }.
% 0.72/1.09  (287) {G1,W9,D2,L2,V1,M1} R(73,46) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Literal ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral )
% 0.72/1.09     }.
% 0.72/1.09  (476) {G3,W9,D2,L2,V1,M1} R(243,77) { iext( X, uri_rdfs_Seq, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (480) {G4,W9,D2,L2,V1,M1} R(479,77) { iext( X, uri_rdfs_label, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (483) {G6,W9,D2,L2,V1,M1} R(482,77) { iext( X, uri_rdfs_label, 
% 0.72/1.09    uri_rdfs_label ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (487) {G3,W9,D2,L2,V1,M1} R(241,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.09  (286) {G1,W9,D2,L2,V1,M1} R(73,45) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Seq ) }.
% 0.72/1.09  (486) {G3,W9,D2,L2,V1,M1} R(241,77) { iext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource ), ! iext( 
% 0.72/1.09    uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (489) {G3,W9,D2,L2,V1,M1} R(239,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Bag ) }.
% 0.72/1.09  (488) {G3,W9,D2,L2,V1,M1} R(239,77) { iext( X, uri_rdf_Bag, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (491) {G3,W9,D2,L2,V1,M1} R(237,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Alt ) }.
% 0.72/1.09  (285) {G1,W9,D2,L2,V1,M1} R(73,33) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.09  (490) {G3,W9,D2,L2,V1,M1} R(237,77) { iext( X, uri_rdf_Alt, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (492) {G5,W9,D2,L2,V1,M1} R(227,77) { iext( X, uri_rdfs_member, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (496) {G4,W9,D2,L2,V1,M1} R(495,77) { iext( X, uri_rdfs_comment, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (499) {G6,W9,D2,L2,V1,M1} R(498,77) { iext( X, uri_rdfs_comment, 
% 0.72/1.09    uri_rdfs_comment ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (284) {G1,W9,D2,L2,V1,M1} R(73,31) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Bag ) }.
% 0.72/1.09  (507) {G5,W9,D2,L2,V1,M1} R(505,77) { iext( X, uri_rdf_List, uri_rdf_List )
% 0.72/1.09    , ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (511) {G5,W9,D2,L2,V1,M1} R(506,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_List ) }.
% 0.72/1.09  (510) {G5,W9,D2,L2,V1,M1} R(506,77) { iext( X, uri_rdf_List, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (512) {G4,W9,D2,L2,V1,M1} R(504,77) { iext( X, uri_rdf_List, uri_rdfs_Class
% 0.72/1.09     ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (283) {G1,W9,D2,L2,V1,M1} R(73,30) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Container ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Alt ) }.
% 0.72/1.09  (518) {G5,W9,D2,L2,V1,M1} R(516,77) { iext( X, uri_rdfs_Statement, 
% 0.72/1.09    uri_rdfs_Statement ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (522) {G5,W9,D2,L2,V1,M1} R(517,73) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdfs_Statement )
% 0.72/1.09     }.
% 0.72/1.09  (521) {G5,W9,D2,L2,V1,M1} R(517,77) { iext( X, uri_rdfs_Statement, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subPropertyOf, uri_rdfs_subClassOf
% 0.72/1.09    , X ) }.
% 0.72/1.09  (523) {G4,W9,D2,L2,V1,M1} R(515,77) { iext( X, uri_rdfs_Statement, 
% 0.72/1.09    uri_rdfs_Class ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (282) {G4,W9,D2,L2,V1,M1} R(73,199) { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.09    uri_rdfs_Resource ), ! iext( uri_rdfs_subClassOf, X, uri_rdf_Property )
% 0.72/1.09     }.
% 0.72/1.09  (526) {G4,W9,D2,L2,V1,M1} R(525,77) { iext( X, uri_rdf_predicate, 
% 0.72/1.09    uri_rdf_Property ), ! iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (529) {G6,W9,D2,L2,V1,M1} R(528,77) { iext( X, uri_rdf_predicate, 
% 0.72/1.09    uri_rdf_predicate ), ! iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (302) {G3,W9,D2,L2,V2,M1} R(77,129) { iext( X, Y, uri_rdfs_Resource ), ! 
% 0.72/1.09    iext( uri_rdfs_subPropertyOf, uri_rdf_type, X ) }.
% 0.72/1.09  (193) {G1,W8,D2,L2,V1,M1} R(51,86) { icext( X, uri_ex_s ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_ex_p, X ) }.
% 0.72/1.09  (192) {G1,W8,D2,L2,V1,M1} R(51,84) { icext( X, uri_rdf_value ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (191) {G1,W8,D2,L2,V1,M1} R(51,83) { icext( X, uri_rdf_value ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (190) {G1,W8,D2,L2,V1,M1} R(51,82) { icext( X, uri_rdf_type ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (188) {G1,W8,D2,L2,V1,M1} R(51,81) { icext( X, uri_rdf_type ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (187) {G1,W8,D2,L2,V1,M1} R(51,78) { icext( X, uri_rdfs_subPropertyOf ), ! 
% 0.72/1.09    iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (186) {G1,W8,D2,L2,V1,M1} R(51,74) { icext( X, uri_rdfs_subPropertyOf ), ! 
% 0.72/1.09    iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (184) {G1,W8,D2,L2,V1,M1} R(51,71) { icext( X, uri_rdfs_subClassOf ), ! 
% 0.72/1.09    iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (183) {G1,W8,D2,L2,V1,M1} R(51,67) { icext( X, uri_rdfs_subClassOf ), ! 
% 0.72/1.09    iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (182) {G1,W8,D2,L2,V1,M1} R(51,66) { icext( X, uri_rdf_subject ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (181) {G1,W8,D2,L2,V1,M1} R(51,65) { icext( X, uri_rdf_subject ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (531) {G6,W8,D2,L2,V1,M1} R(528,51) { icext( X, uri_rdf_predicate ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (530) {G6,W8,D2,L2,V1,M1} R(528,60) { icext( X, uri_rdf_predicate ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (179) {G1,W8,D2,L2,V1,M1} R(51,64) { icext( X, uri_rdf_predicate ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (528) {G5,W4,D2,L1,V0,M1} R(527,79) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.09    uri_rdf_predicate, uri_rdf_predicate ) }.
% 0.72/1.09  (527) {G4,W2,D2,L1,V0,M1} R(525,11) { ip( uri_rdf_predicate ) }.
% 0.72/1.09  (525) {G3,W4,D2,L1,V0,M1} R(524,24) { iext( uri_rdf_type, uri_rdf_predicate
% 0.72/1.09    , uri_rdf_Property ) }.
% 0.72/1.09  (524) {G2,W3,D2,L1,V0,M1} R(178,59) { icext( uri_rdf_Property, 
% 0.72/1.09    uri_rdf_predicate ) }.
% 0.72/1.09  (178) {G1,W8,D2,L2,V1,M1} R(51,63) { icext( X, uri_rdf_predicate ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (177) {G1,W8,D2,L2,V1,M1} R(51,62) { icext( X, uri_rdf_object ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (176) {G1,W8,D2,L2,V1,M1} R(51,61) { icext( X, uri_rdfs_range ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (175) {G1,W8,D2,L2,V1,M1} R(51,59) { icext( X, uri_rdfs_range ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (173) {G1,W8,D2,L2,V1,M1} R(51,52) { icext( X, uri_rdfs_domain ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (172) {G1,W8,D2,L2,V1,M1} R(51,49) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (170) {G1,W8,D2,L2,V1,M1} R(51,46) { icext( X, uri_rdf_XMLLiteral ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (169) {G1,W8,D2,L2,V1,M1} R(51,45) { icext( X, uri_rdfs_Seq ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (164) {G1,W8,D2,L2,V1,M1} R(51,41) { icext( X, uri_rdf__3 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (163) {G1,W8,D2,L2,V1,M1} R(51,40) { icext( X, uri_rdf__2 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (195) {G3,W8,D2,L2,V1,M1} R(130,51) { icext( X, uri_rdf__3 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (196) {G3,W8,D2,L2,V1,M1} R(131,51) { icext( X, uri_rdf__2 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (197) {G3,W8,D2,L2,V1,M1} R(132,51) { icext( X, uri_rdf__1 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (200) {G4,W8,D2,L2,V1,M1} R(199,51) { icext( X, uri_rdf_Property ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (162) {G1,W8,D2,L2,V1,M1} R(51,39) { icext( X, uri_rdf__1 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (224) {G1,W8,D2,L2,V1,M1} R(60,86) { icext( X, uri_ex_o ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_ex_p, X ) }.
% 0.72/1.09  (223) {G1,W8,D2,L2,V1,M1} R(60,78) { icext( X, uri_rdf_Property ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.72/1.09  (222) {G1,W8,D2,L2,V1,M1} R(60,3) { icext( X, uri_rdf_List ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdf_type, X ) }.
% 0.72/1.09  (221) {G1,W8,D2,L2,V1,M1} R(60,67) { icext( X, uri_rdfs_Class ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.72/1.09  (161) {G1,W8,D2,L2,V1,M1} R(51,38) { icext( X, uri_rdf__3 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (520) {G5,W8,D2,L2,V1,M1} R(516,51) { icext( X, uri_rdfs_Statement ), ! 
% 0.72/1.09    iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (519) {G5,W8,D2,L2,V1,M1} R(516,60) { icext( X, uri_rdfs_Statement ), ! 
% 0.72/1.09    iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (515) {G3,W4,D2,L1,V0,M1} R(513,24) { iext( uri_rdf_type, 
% 0.72/1.09    uri_rdfs_Statement, uri_rdfs_Class ) }.
% 0.72/1.09  (517) {G4,W4,D2,L1,V0,M1} R(514,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdfs_Statement, uri_rdfs_Resource ) }.
% 0.72/1.09  (516) {G4,W4,D2,L1,V0,M1} R(514,72) { iext( uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdfs_Statement, uri_rdfs_Statement ) }.
% 0.72/1.09  (514) {G3,W2,D2,L1,V0,M1} R(513,54) { ic( uri_rdfs_Statement ) }.
% 0.72/1.09  (513) {G2,W3,D2,L1,V0,M1} R(220,52) { icext( uri_rdfs_Class, 
% 0.72/1.09    uri_rdfs_Statement ) }.
% 0.72/1.09  (220) {G1,W8,D2,L2,V1,M1} R(60,62) { icext( X, uri_rdfs_Statement ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.72/1.09  (159) {G1,W8,D2,L2,V1,M1} R(51,37) { icext( X, uri_rdf__2 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (219) {G1,W8,D2,L2,V1,M1} R(60,58) { icext( X, uri_rdfs_Class ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdf_type, X ) }.
% 0.72/1.09  (218) {G1,W8,D2,L2,V1,M1} R(60,52) { icext( X, uri_rdfs_Class ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.72/1.09  (217) {G1,W8,D2,L2,V1,M1} R(60,50) { icext( X, uri_rdf_Property ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.72/1.09  (216) {G1,W8,D2,L2,V1,M1} R(60,49) { icext( X, uri_rdfs_Class ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (158) {G1,W8,D2,L2,V1,M1} R(51,36) { icext( X, uri_rdf__1 ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (215) {G1,W8,D2,L2,V1,M1} R(60,47) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.72/1.09  (214) {G1,W8,D2,L2,V1,M1} R(60,46) { icext( X, uri_rdfs_Literal ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (213) {G1,W8,D2,L2,V1,M1} R(60,42) { icext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_range, 
% 0.72/1.09    uri_rdf_type, X ) }.
% 0.72/1.09  (212) {G1,W8,D2,L2,V1,M1} R(60,33) { icext( X, uri_rdf_Property ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (157) {G1,W8,D2,L2,V1,M1} R(51,35) { icext( X, uri_rdfs_member ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (211) {G1,W8,D2,L2,V1,M1} R(60,30) { icext( X, uri_rdfs_Container ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (210) {G1,W8,D2,L2,V1,M1} R(60,29) { icext( X, uri_rdf_List ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.72/1.09  (509) {G5,W8,D2,L2,V1,M1} R(505,51) { icext( X, uri_rdf_List ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (508) {G5,W8,D2,L2,V1,M1} R(505,60) { icext( X, uri_rdf_List ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (156) {G1,W8,D2,L2,V1,M1} R(51,34) { icext( X, uri_rdfs_member ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.09  (504) {G3,W4,D2,L1,V0,M1} R(502,24) { iext( uri_rdf_type, uri_rdf_List, 
% 0.72/1.09    uri_rdfs_Class ) }.
% 0.72/1.09  (506) {G4,W4,D2,L1,V0,M1} R(503,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdf_List, uri_rdfs_Resource ) }.
% 0.72/1.09  (505) {G4,W4,D2,L1,V0,M1} R(503,72) { iext( uri_rdfs_subClassOf, 
% 0.72/1.09    uri_rdf_List, uri_rdf_List ) }.
% 0.72/1.09  (503) {G3,W2,D2,L1,V0,M1} R(502,54) { ic( uri_rdf_List ) }.
% 0.72/1.09  (502) {G2,W3,D2,L1,V0,M1} R(209,52) { icext( uri_rdfs_Class, uri_rdf_List )
% 0.72/1.09     }.
% 0.72/1.09  (209) {G1,W8,D2,L2,V1,M1} R(60,26) { icext( X, uri_rdf_List ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.72/1.09  (208) {G1,W8,D2,L2,V1,M1} R(60,20) { icext( X, uri_rdfs_Literal ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.72/1.09  (207) {G1,W8,D2,L2,V1,M1} R(60,18) { icext( X, uri_rdfs_seeAlso ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (154) {G1,W8,D2,L2,V1,M1} R(51,33) { icext( X, 
% 0.72/1.09    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_domain, 
% 0.72/1.09    uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (206) {G1,W8,D2,L2,V1,M1} R(60,16) { icext( X, uri_rdfs_Resource ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_domain, X ) }.
% 0.72/1.09  (205) {G3,W8,D2,L2,V1,M1} R(60,108) { icext( X, uri_rdf_Property ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.72/1.09  (204) {G1,W8,D2,L2,V1,M1} R(60,17) { icext( X, uri_rdfs_Resource ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_range, X ) }.
% 0.72/1.09  (203) {G3,W8,D2,L2,V1,M1} R(60,129) { icext( X, uri_rdfs_Resource ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdf_type, X ) }.
% 0.72/1.09  (153) {G1,W8,D2,L2,V1,M1} R(51,31) { icext( X, uri_rdf_Bag ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (202) {G3,W8,D2,L2,V1,M1} R(60,132) { icext( X, uri_rdfs_member ), ! iext( 
% 0.72/1.09    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (201) {G4,W8,D2,L2,V1,M1} R(60,199) { icext( X, uri_rdfs_Resource ), ! iext
% 0.72/1.09    ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (390) {G3,W8,D2,L2,V1,M1} R(372,60) { icext( X, uri_rdfs_isDefinedBy ), ! 
% 0.72/1.09    iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (392) {G3,W8,D2,L2,V1,M1} R(373,51) { icext( X, uri_rdfs_seeAlso ), ! iext
% 0.72/1.09    ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (152) {G1,W8,D2,L2,V1,M1} R(51,30) { icext( X, uri_rdf_Alt ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.09  (394) {G5,W8,D2,L2,V1,M1} R(374,51) { icext( X, uri_rdfs_member ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (397) {G3,W8,D2,L2,V1,M1} R(375,51) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.72/1.09     iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (396) {G3,W8,D2,L2,V1,M1} R(375,60) { icext( X, uri_rdfs_subPropertyOf ), !
% 0.72/1.09     iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (404) {G3,W8,D2,L2,V1,M1} R(376,51) { icext( X, uri_rdf_first ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.09  (151) {G1,W8,D2,L2,V1,M1} R(51,29) { icext( X, uri_rdf_rest ), ! iext( 
% 0.72/1.09    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.09  (403) {G3,W8,D2,L2,V1,M1} R(376,60) { icext( X, uri_rdf_first ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (407) {G3,W8,D2,L2,V1,M1} R(377,51) { icext( X, uri_rdf_rest ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (406) {G3,W8,D2,L2,V1,M1} R(377,60) { icext( X, uri_rdf_rest ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (409) {G3,W8,D2,L2,V1,M1} R(378,60) { icext( X, uri_rdf__1 ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (411) {G3,W8,D2,L2,V1,M1} R(379,60) { icext( X, uri_rdf__2 ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (414) {G3,W8,D2,L2,V1,M1} R(380,60) { icext( X, uri_rdf__3 ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (417) {G3,W8,D2,L2,V1,M1} R(381,51) { icext( X, uri_rdf_object ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (416) {G3,W8,D2,L2,V1,M1} R(381,60) { icext( X, uri_rdf_object ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (420) {G3,W8,D2,L2,V1,M1} R(382,51) { icext( X, uri_rdf_value ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (419) {G3,W8,D2,L2,V1,M1} R(382,60) { icext( X, uri_rdf_value ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (423) {G3,W8,D2,L2,V1,M1} R(383,51) { icext( X, uri_rdf_subject ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (422) {G3,W8,D2,L2,V1,M1} R(383,60) { icext( X, uri_rdf_subject ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (426) {G3,W8,D2,L2,V1,M1} R(384,51) { icext( X, uri_rdfs_subClassOf ), ! 
% 0.72/1.10    iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (425) {G3,W8,D2,L2,V1,M1} R(384,60) { icext( X, uri_rdfs_subClassOf ), ! 
% 0.72/1.10    iext( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (429) {G3,W8,D2,L2,V1,M1} R(385,51) { icext( X, uri_rdf_type ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (428) {G3,W8,D2,L2,V1,M1} R(385,60) { icext( X, uri_rdf_type ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (432) {G3,W8,D2,L2,V1,M1} R(386,51) { icext( X, uri_ex_p ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (431) {G3,W8,D2,L2,V1,M1} R(386,60) { icext( X, uri_ex_p ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (435) {G3,W8,D2,L2,V1,M1} R(387,51) { icext( X, uri_rdfs_range ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (434) {G3,W8,D2,L2,V1,M1} R(387,60) { icext( X, uri_rdfs_range ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (438) {G3,W8,D2,L2,V1,M1} R(388,51) { icext( X, uri_rdfs_domain ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (437) {G3,W8,D2,L2,V1,M1} R(388,60) { icext( X, uri_rdfs_domain ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (444) {G3,W8,D2,L2,V1,M1} R(268,60) { icext( X, uri_rdfs_Datatype ), ! iext
% 0.72/1.10    ( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (446) {G3,W8,D2,L2,V1,M1} R(269,60) { icext( X, uri_rdf_XMLLiteral ), ! 
% 0.72/1.10    iext( uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (145) {G1,W8,D2,L2,V1,M1} R(51,14) { icext( X, uri_rdfs_comment ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (448) {G3,W8,D2,L2,V1,M1} R(270,51) { icext( X, uri_rdfs_Class ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (450) {G3,W8,D2,L2,V1,M1} R(271,51) { icext( X, uri_rdfs_Literal ), ! iext
% 0.72/1.10    ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (452) {G3,W8,D2,L2,V1,M1} R(272,51) { icext( X, uri_rdfs_Container ), ! 
% 0.72/1.10    iext( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (454) {G3,W8,D2,L2,V1,M1} R(273,60) { icext( X, uri_rdfs_Seq ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (144) {G1,W8,D2,L2,V1,M1} R(51,28) { icext( X, uri_rdf_rest ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (456) {G3,W8,D2,L2,V1,M1} R(274,60) { icext( X, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ), ! iext( uri_rdfs_range, 
% 0.72/1.10    uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (458) {G3,W8,D2,L2,V1,M1} R(275,60) { icext( X, uri_rdf_Bag ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (460) {G3,W8,D2,L2,V1,M1} R(276,60) { icext( X, uri_rdf_Alt ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (475) {G6,W8,D2,L2,V1,M1} R(249,51) { icext( X, uri_rdfs_Resource ), ! iext
% 0.72/1.10    ( uri_rdfs_domain, uri_rdfs_subClassOf, X ) }.
% 0.72/1.10  (143) {G1,W8,D2,L2,V1,M1} R(51,27) { icext( X, uri_rdf_first ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.10  (485) {G6,W8,D2,L2,V1,M1} R(482,51) { icext( X, uri_rdfs_label ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (484) {G6,W8,D2,L2,V1,M1} R(482,60) { icext( X, uri_rdfs_label ), ! iext( 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (501) {G6,W8,D2,L2,V1,M1} R(498,51) { icext( X, uri_rdfs_comment ), ! iext
% 0.72/1.10    ( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (500) {G6,W8,D2,L2,V1,M1} R(498,60) { icext( X, uri_rdfs_comment ), ! iext
% 0.72/1.10    ( uri_rdfs_range, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (142) {G1,W8,D2,L2,V1,M1} R(51,26) { icext( X, uri_rdf_first ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (194) {G3,W8,D2,L2,V2,M1} R(129,51) { icext( X, Y ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdf_type, X ) }.
% 0.72/1.10  (261) {G1,W7,D2,L2,V1,M1} R(70,49) { icext( uri_rdfs_Class, X ), ! icext( 
% 0.72/1.10    uri_rdfs_Datatype, X ) }.
% 0.72/1.10  (260) {G1,W7,D2,L2,V1,M1} R(70,46) { icext( uri_rdfs_Literal, X ), ! icext
% 0.72/1.10    ( uri_rdf_XMLLiteral, X ) }.
% 0.72/1.10  (259) {G1,W7,D2,L2,V1,M1} R(70,45) { icext( uri_rdfs_Container, X ), ! 
% 0.72/1.10    icext( uri_rdfs_Seq, X ) }.
% 0.72/1.10  (141) {G1,W8,D2,L2,V1,M1} R(51,22) { icext( X, uri_rdfs_seeAlso ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.10  (498) {G5,W4,D2,L1,V0,M1} R(497,79) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_comment, uri_rdfs_comment ) }.
% 0.72/1.10  (497) {G4,W2,D2,L1,V0,M1} R(495,11) { ip( uri_rdfs_comment ) }.
% 0.72/1.10  (495) {G3,W4,D2,L1,V0,M1} R(494,24) { iext( uri_rdf_type, uri_rdfs_comment
% 0.72/1.10    , uri_rdf_Property ) }.
% 0.72/1.10  (494) {G2,W3,D2,L1,V0,M1} R(140,59) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_comment ) }.
% 0.72/1.10  (140) {G1,W8,D2,L2,V1,M1} R(51,15) { icext( X, uri_rdfs_comment ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.10  (258) {G1,W7,D2,L2,V1,M1} R(70,33) { icext( uri_rdf_Property, X ), ! icext
% 0.72/1.10    ( uri_rdfs_ContainerMembershipProperty, X ) }.
% 0.72/1.10  (257) {G1,W7,D2,L2,V1,M1} R(70,31) { icext( uri_rdfs_Container, X ), ! 
% 0.72/1.10    icext( uri_rdf_Bag, X ) }.
% 0.72/1.10  (256) {G1,W7,D2,L2,V1,M1} R(70,30) { icext( uri_rdfs_Container, X ), ! 
% 0.72/1.10    icext( uri_rdf_Alt, X ) }.
% 0.72/1.10  (493) {G5,W3,D2,L1,V0,M1} R(227,23) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_member ) }.
% 0.72/1.10  (139) {G1,W8,D2,L2,V1,M1} R(51,21) { icext( X, uri_rdfs_seeAlso ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (227) {G4,W4,D2,L1,V0,M1} R(225,12) { iext( uri_rdf_type, uri_rdfs_member, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (237) {G2,W4,D2,L1,V0,M1} R(230,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Alt, uri_rdfs_Resource ) }.
% 0.72/1.10  (239) {G2,W4,D2,L1,V0,M1} R(231,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Bag, uri_rdfs_Resource ) }.
% 0.72/1.10  (241) {G2,W4,D2,L1,V0,M1} R(232,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource ) }.
% 0.72/1.10  (138) {G1,W8,D2,L2,V1,M1} R(51,20) { icext( X, uri_rdfs_label ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.10  (482) {G5,W4,D2,L1,V0,M1} R(481,79) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_label, uri_rdfs_label ) }.
% 0.72/1.10  (481) {G4,W2,D2,L1,V0,M1} R(479,11) { ip( uri_rdfs_label ) }.
% 0.72/1.10  (479) {G3,W4,D2,L1,V0,M1} R(478,24) { iext( uri_rdf_type, uri_rdfs_label, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (478) {G2,W3,D2,L1,V0,M1} R(137,50) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_label ) }.
% 0.72/1.10  (137) {G1,W8,D2,L2,V1,M1} R(51,19) { icext( X, uri_rdfs_label ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (243) {G2,W4,D2,L1,V0,M1} R(233,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Seq, uri_rdfs_Resource ) }.
% 0.72/1.10  (249) {G5,W4,D2,L1,V0,M1} R(244,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Resource, uri_rdfs_Resource ) }.
% 0.72/1.10  (251) {G2,W4,D2,L1,V0,M1} R(245,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Container, uri_rdfs_Resource ) }.
% 0.72/1.10  (253) {G2,W4,D2,L1,V0,M1} R(246,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Literal, uri_rdfs_Resource ) }.
% 0.72/1.10  (136) {G1,W8,D2,L2,V1,M1} R(51,18) { icext( X, uri_rdfs_isDefinedBy ), ! 
% 0.72/1.10    iext( uri_rdfs_domain, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (255) {G2,W4,D2,L1,V0,M1} R(247,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Class, uri_rdfs_Resource ) }.
% 0.72/1.10  (263) {G2,W4,D2,L1,V0,M1} R(234,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_XMLLiteral, uri_rdfs_Resource ) }.
% 0.72/1.10  (265) {G2,W4,D2,L1,V0,M1} R(235,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Datatype, uri_rdfs_Resource ) }.
% 0.72/1.10  (266) {G3,W4,D2,L1,V0,M1} R(264,24) { iext( uri_rdf_type, uri_rdfs_Datatype
% 0.72/1.10    , uri_rdfs_Class ) }.
% 0.72/1.10  (135) {G1,W8,D2,L2,V1,M1} R(51,16) { icext( X, uri_rdfs_isDefinedBy ), ! 
% 0.72/1.10    iext( uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (267) {G3,W4,D2,L1,V0,M1} R(262,24) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdf_XMLLiteral, uri_rdfs_Class ) }.
% 0.72/1.10  (277) {G3,W4,D2,L1,V0,M1} R(72,198) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Property, uri_rdf_Property ) }.
% 0.72/1.10  (276) {G2,W4,D2,L1,V0,M1} R(72,230) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Alt, uri_rdf_Alt ) }.
% 0.72/1.10  (275) {G2,W4,D2,L1,V0,M1} R(72,231) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Bag, uri_rdf_Bag ) }.
% 0.72/1.10  (274) {G2,W4,D2,L1,V0,M1} R(72,232) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (273) {G2,W4,D2,L1,V0,M1} R(72,233) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Seq, uri_rdfs_Seq ) }.
% 0.72/1.10  (272) {G2,W4,D2,L1,V0,M1} R(72,245) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Container, uri_rdfs_Container ) }.
% 0.72/1.10  (271) {G2,W4,D2,L1,V0,M1} R(72,246) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Literal, uri_rdfs_Literal ) }.
% 0.72/1.10  (133) {G1,W8,D2,L2,V1,M1} R(51,17) { icext( X, uri_rdfs_isDefinedBy ), ! 
% 0.72/1.10    iext( uri_rdfs_domain, uri_rdfs_range, X ) }.
% 0.72/1.10  (270) {G2,W4,D2,L1,V0,M1} R(72,247) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Class, uri_rdfs_Class ) }.
% 0.72/1.10  (269) {G2,W4,D2,L1,V0,M1} R(72,234) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_XMLLiteral, uri_rdf_XMLLiteral ) }.
% 0.72/1.10  (268) {G2,W4,D2,L1,V0,M1} R(72,235) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Datatype, uri_rdfs_Datatype ) }.
% 0.72/1.10  (278) {G3,W4,D2,L1,V0,M1} R(254,24) { iext( uri_rdf_type, uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (89) {G1,W9,D2,L2,V1,M1} F(77) { iext( X, uri_rdfs_subPropertyOf, X ), ! 
% 0.72/1.10    iext( uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X ) }.
% 0.72/1.10  (279) {G3,W4,D2,L1,V0,M1} R(252,24) { iext( uri_rdf_type, uri_rdfs_Literal
% 0.72/1.10    , uri_rdfs_Class ) }.
% 0.72/1.10  (280) {G3,W4,D2,L1,V0,M1} R(250,24) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdfs_Container, uri_rdfs_Class ) }.
% 0.72/1.10  (281) {G6,W4,D2,L1,V0,M1} R(248,24) { iext( uri_rdf_type, uri_rdfs_Resource
% 0.72/1.10    , uri_rdfs_Class ) }.
% 0.72/1.10  (388) {G2,W4,D2,L1,V0,M1} R(79,90) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain ) }.
% 0.72/1.10  (88) {G1,W8,D2,L2,V1,M1} F(60) { icext( X, X ), ! iext( uri_rdfs_range, 
% 0.72/1.10    uri_rdfs_range, X ) }.
% 0.72/1.10  (387) {G2,W4,D2,L1,V0,M1} R(79,91) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_range, uri_rdfs_range ) }.
% 0.72/1.10  (386) {G2,W4,D2,L1,V0,M1} R(79,92) { iext( uri_rdfs_subPropertyOf, uri_ex_p
% 0.72/1.10    , uri_ex_p ) }.
% 0.72/1.10  (385) {G2,W4,D2,L1,V0,M1} R(79,93) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_type, uri_rdf_type ) }.
% 0.72/1.10  (384) {G2,W4,D2,L1,V0,M1} R(79,94) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_subClassOf, uri_rdfs_subClassOf ) }.
% 0.72/1.10  (87) {G1,W8,D2,L2,V1,M1} F(51) { icext( X, uri_rdfs_domain ), ! iext( 
% 0.72/1.10    uri_rdfs_domain, uri_rdfs_domain, X ) }.
% 0.72/1.10  (383) {G2,W4,D2,L1,V0,M1} R(79,95) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_subject, uri_rdf_subject ) }.
% 0.72/1.10  (382) {G2,W4,D2,L1,V0,M1} R(79,96) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_value, uri_rdf_value ) }.
% 0.72/1.10  (381) {G2,W4,D2,L1,V0,M1} R(79,97) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_object, uri_rdf_object ) }.
% 0.72/1.10  (380) {G2,W4,D2,L1,V0,M1} R(79,98) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__3, uri_rdf__3 ) }.
% 0.72/1.10  (379) {G2,W4,D2,L1,V0,M1} R(79,99) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__2, uri_rdf__2 ) }.
% 0.72/1.10  (378) {G2,W4,D2,L1,V0,M1} R(79,100) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__1, uri_rdf__1 ) }.
% 0.72/1.10  (377) {G2,W4,D2,L1,V0,M1} R(79,101) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_rest, uri_rdf_rest ) }.
% 0.72/1.10  (376) {G2,W4,D2,L1,V0,M1} R(79,102) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_first, uri_rdf_first ) }.
% 0.72/1.10  (80) {G0,W14,D2,L3,V3,M1} I { ! iext( uri_rdfs_subPropertyOf, X, Z ), iext
% 0.72/1.10    ( uri_rdfs_subPropertyOf, X, Y ), ! iext( uri_rdfs_subPropertyOf, Z, Y )
% 0.72/1.10     }.
% 0.72/1.10  (375) {G2,W4,D2,L1,V0,M1} R(79,107) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf ) }.
% 0.72/1.10  (374) {G4,W4,D2,L1,V0,M1} R(79,225) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_member, uri_rdfs_member ) }.
% 0.72/1.10  (373) {G2,W4,D2,L1,V0,M1} R(79,226) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_seeAlso, uri_rdfs_seeAlso ) }.
% 0.72/1.10  (372) {G2,W4,D2,L1,V0,M1} R(79,293) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy ) }.
% 0.72/1.10  (79) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subPropertyOf, X, X ), ! ip( X
% 0.72/1.10     ) }.
% 0.72/1.10  (289) {G3,W4,D2,L1,V0,M1} R(242,24) { iext( uri_rdf_type, uri_rdfs_Seq, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (290) {G3,W4,D2,L1,V0,M1} R(240,24) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class ) }.
% 0.72/1.10  (291) {G3,W4,D2,L1,V0,M1} R(238,24) { iext( uri_rdf_type, uri_rdf_Bag, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (292) {G3,W4,D2,L1,V0,M1} R(236,24) { iext( uri_rdf_type, uri_rdf_Alt, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (77) {G0,W14,D2,L3,V4,M1} I { ! iext( uri_rdfs_subPropertyOf, X, Y ), iext
% 0.72/1.10    ( Y, Z, T ), ! iext( X, Z, T ) }.
% 0.72/1.10  (295) {G3,W3,D2,L1,V0,M1} R(294,23) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_isDefinedBy ) }.
% 0.72/1.10  (294) {G2,W4,D2,L1,V0,M1} R(293,12) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdfs_isDefinedBy, uri_rdf_Property ) }.
% 0.72/1.10  (229) {G3,W3,D2,L1,V0,M1} R(228,23) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_seeAlso ) }.
% 0.72/1.10  (293) {G1,W2,D2,L1,V0,M1} R(75,18) { ip( uri_rdfs_isDefinedBy ) }.
% 0.72/1.10  (75) {G0,W7,D2,L2,V2,M1} I { ip( X ), ! iext( uri_rdfs_subPropertyOf, X, Y
% 0.72/1.10     ) }.
% 0.72/1.10  (236) {G2,W3,D2,L1,V0,M1} R(230,53) { icext( uri_rdfs_Class, uri_rdf_Alt )
% 0.72/1.10     }.
% 0.72/1.10  (238) {G2,W3,D2,L1,V0,M1} R(231,53) { icext( uri_rdfs_Class, uri_rdf_Bag )
% 0.72/1.10     }.
% 0.72/1.10  (240) {G2,W3,D2,L1,V0,M1} R(232,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (242) {G2,W3,D2,L1,V0,M1} R(233,53) { icext( uri_rdfs_Class, uri_rdfs_Seq )
% 0.72/1.10     }.
% 0.72/1.10  (73) {G0,W14,D2,L3,V3,M1} I { ! iext( uri_rdfs_subClassOf, X, Z ), iext( 
% 0.72/1.10    uri_rdfs_subClassOf, X, Y ), ! iext( uri_rdfs_subClassOf, Z, Y ) }.
% 0.72/1.10  (248) {G5,W3,D2,L1,V0,M1} R(244,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (250) {G2,W3,D2,L1,V0,M1} R(245,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_Container ) }.
% 0.72/1.10  (252) {G2,W3,D2,L1,V0,M1} R(246,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_Literal ) }.
% 0.72/1.10  (254) {G2,W3,D2,L1,V0,M1} R(247,53) { icext( uri_rdfs_Class, uri_rdfs_Class
% 0.72/1.10     ) }.
% 0.72/1.10  (72) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X, X ), ! ic( X )
% 0.72/1.10     }.
% 0.72/1.10  (262) {G2,W3,D2,L1,V0,M1} R(234,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdf_XMLLiteral ) }.
% 0.72/1.10  (264) {G2,W3,D2,L1,V0,M1} R(235,53) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdfs_Datatype ) }.
% 0.72/1.10  (235) {G1,W2,D2,L1,V0,M1} R(68,49) { ic( uri_rdfs_Datatype ) }.
% 0.72/1.10  (234) {G1,W2,D2,L1,V0,M1} R(68,46) { ic( uri_rdf_XMLLiteral ) }.
% 0.72/1.10  (70) {G0,W12,D2,L3,V3,M1} I { ! icext( X, Z ), icext( Y, Z ), ! iext( 
% 0.72/1.10    uri_rdfs_subClassOf, X, Y ) }.
% 0.72/1.10  (247) {G1,W2,D2,L1,V0,M1} R(69,49) { ic( uri_rdfs_Class ) }.
% 0.72/1.10  (246) {G1,W2,D2,L1,V0,M1} R(69,46) { ic( uri_rdfs_Literal ) }.
% 0.72/1.10  (245) {G1,W2,D2,L1,V0,M1} R(69,30) { ic( uri_rdfs_Container ) }.
% 0.72/1.10  (244) {G4,W2,D2,L1,V0,M1} R(69,199) { ic( uri_rdfs_Resource ) }.
% 0.72/1.10  (69) {G0,W7,D2,L2,V2,M1} I { ic( Y ), ! iext( uri_rdfs_subClassOf, X, Y )
% 0.72/1.10     }.
% 0.72/1.10  (233) {G1,W2,D2,L1,V0,M1} R(68,45) { ic( uri_rdfs_Seq ) }.
% 0.72/1.10  (232) {G1,W2,D2,L1,V0,M1} R(68,33) { ic( 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (231) {G1,W2,D2,L1,V0,M1} R(68,31) { ic( uri_rdf_Bag ) }.
% 0.72/1.10  (230) {G1,W2,D2,L1,V0,M1} R(68,30) { ic( uri_rdf_Alt ) }.
% 0.72/1.10  (68) {G0,W7,D2,L2,V2,M1} I { ic( X ), ! iext( uri_rdfs_subClassOf, X, Y )
% 0.72/1.10     }.
% 0.72/1.10  (228) {G2,W4,D2,L1,V0,M1} R(226,12) { iext( uri_rdf_type, uri_rdfs_seeAlso
% 0.72/1.10    , uri_rdf_Property ) }.
% 0.72/1.10  (226) {G1,W2,D2,L1,V0,M1} R(76,18) { ip( uri_rdfs_seeAlso ) }.
% 0.72/1.10  (225) {G3,W2,D2,L1,V0,M1} R(76,132) { ip( uri_rdfs_member ) }.
% 0.72/1.10  (76) {G0,W7,D2,L2,V2,M1} I { ip( Y ), ! iext( uri_rdfs_subPropertyOf, X, Y
% 0.72/1.10     ) }.
% 0.72/1.10  (60) {G0,W13,D2,L3,V4,M1} I { icext( X, Y ), ! iext( uri_rdfs_range, Z, X )
% 0.72/1.10    , ! iext( Z, T, Y ) }.
% 0.72/1.10  (199) {G3,W4,D2,L1,V0,M1} R(198,25) { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdf_Property, uri_rdfs_Resource ) }.
% 0.72/1.10  (198) {G2,W2,D2,L1,V0,M1} R(54,124) { ic( uri_rdf_Property ) }.
% 0.72/1.10  (54) {G0,W6,D2,L2,V1,M1} I { ic( X ), ! icext( uri_rdfs_Class, X ) }.
% 0.72/1.10  (56) {G0,W6,D2,L2,V1,M1} I { icext( uri_rdfs_Literal, X ), ! lv( X ) }.
% 0.72/1.10  (53) {G0,W6,D2,L2,V1,M1} I { icext( uri_rdfs_Class, X ), ! ic( X ) }.
% 0.72/1.10  (132) {G2,W4,D2,L1,V0,M1} R(32,118) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__1, uri_rdfs_member ) }.
% 0.72/1.10  (131) {G2,W4,D2,L1,V0,M1} R(32,119) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__2, uri_rdfs_member ) }.
% 0.72/1.10  (130) {G2,W4,D2,L1,V0,M1} R(32,120) { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf__3, uri_rdfs_member ) }.
% 0.72/1.10  (129) {G2,W4,D2,L1,V1,M1} R(24,55) { iext( uri_rdf_type, X, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (51) {G0,W13,D2,L3,V4,M1} I { icext( X, Y ), ! iext( uri_rdfs_domain, Z, X
% 0.72/1.10     ), ! iext( Z, Y, T ) }.
% 0.72/1.10  (128) {G1,W3,D2,L1,V0,M1} R(23,2) { icext( uri_rdf_Property, uri_rdf_first
% 0.72/1.10     ) }.
% 0.72/1.10  (127) {G1,W3,D2,L1,V0,M1} R(23,3) { icext( uri_rdf_List, uri_rdf_nil ) }.
% 0.72/1.10  (126) {G1,W3,D2,L1,V0,M1} R(23,4) { icext( uri_rdf_Property, uri_rdf_rest )
% 0.72/1.10     }.
% 0.72/1.10  (125) {G1,W3,D2,L1,V0,M1} R(23,5) { icext( uri_rdf_Property, uri_rdf__1 )
% 0.72/1.10     }.
% 0.72/1.10  (48) {G0,W8,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X, uri_rdfs_Literal
% 0.72/1.10     ), ! icext( uri_rdfs_Datatype, X ) }.
% 0.72/1.10  (124) {G1,W3,D2,L1,V0,M1} R(23,58) { icext( uri_rdfs_Class, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (123) {G1,W3,D2,L1,V0,M1} R(23,6) { icext( uri_rdf_Property, uri_rdf__2 )
% 0.72/1.10     }.
% 0.72/1.10  (122) {G1,W3,D2,L1,V0,M1} R(23,47) { icext( uri_rdfs_Datatype, 
% 0.72/1.10    uri_rdf_XMLLiteral ) }.
% 0.72/1.10  (121) {G1,W3,D2,L1,V0,M1} R(23,7) { icext( uri_rdf_Property, uri_rdf__3 )
% 0.72/1.10     }.
% 0.72/1.10  (32) {G0,W8,D2,L2,V1,M1} I { iext( uri_rdfs_subPropertyOf, X, 
% 0.72/1.10    uri_rdfs_member ), ! icext( uri_rdfs_ContainerMembershipProperty, X ) }.
% 0.72/1.10  (120) {G1,W3,D2,L1,V0,M1} R(23,44) { icext( 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdf__3 ) }.
% 0.72/1.10  (119) {G1,W3,D2,L1,V0,M1} R(23,43) { icext( 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdf__2 ) }.
% 0.72/1.10  (118) {G1,W3,D2,L1,V0,M1} R(23,42) { icext( 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdf__1 ) }.
% 0.72/1.10  (117) {G1,W3,D2,L1,V0,M1} R(23,8) { icext( uri_rdf_Property, uri_rdf_object
% 0.72/1.10     ) }.
% 0.72/1.10  (25) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdfs_subClassOf, X, 
% 0.72/1.10    uri_rdfs_Resource ), ! ic( X ) }.
% 0.72/1.10  (116) {G1,W3,D2,L1,V0,M1} R(23,9) { icext( uri_rdf_Property, uri_rdf_value
% 0.72/1.10     ) }.
% 0.72/1.10  (115) {G1,W3,D2,L1,V0,M1} R(23,10) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdf_subject ) }.
% 0.72/1.10  (114) {G1,W3,D2,L1,V0,M1} R(23,13) { icext( uri_rdf_Property, uri_rdf_type
% 0.72/1.10     ) }.
% 0.72/1.10  (113) {G3,W3,D2,L1,V0,M1} R(23,103) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_subClassOf ) }.
% 0.72/1.10  (24) {G0,W8,D2,L2,V2,M1} I { iext( uri_rdf_type, X, Y ), ! icext( Y, X )
% 0.72/1.10     }.
% 0.72/1.10  (112) {G3,W3,D2,L1,V0,M1} R(23,104) { icext( uri_rdf_Property, uri_ex_p )
% 0.72/1.10     }.
% 0.72/1.10  (111) {G3,W3,D2,L1,V0,M1} R(23,105) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_range ) }.
% 0.72/1.10  (110) {G3,W3,D2,L1,V0,M1} R(23,106) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_domain ) }.
% 0.72/1.10  (109) {G3,W3,D2,L1,V0,M1} R(23,108) { icext( uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_subPropertyOf ) }.
% 0.72/1.10  (23) {G0,W8,D2,L2,V2,M1} I { icext( Y, X ), ! iext( uri_rdf_type, X, Y )
% 0.72/1.10     }.
% 0.72/1.10  (57) {G0,W6,D2,L2,V1,M1} I { lv( X ), ! icext( uri_rdfs_Literal, X ) }.
% 0.72/1.10  (17) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_isDefinedBy, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (108) {G2,W4,D2,L1,V0,M1} R(107,12) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdfs_subPropertyOf, uri_rdf_Property ) }.
% 0.72/1.10  (107) {G1,W2,D2,L1,V0,M1} R(18,0) { ip( uri_rdfs_subPropertyOf ) }.
% 0.72/1.10  (16) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_isDefinedBy, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (18) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdfs_isDefinedBy, uri_rdfs_seeAlso ) }.
% 0.72/1.10  (19) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_label, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (20) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_label, 
% 0.72/1.10    uri_rdfs_Literal ) }.
% 0.72/1.10  (21) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_seeAlso, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (15) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_comment, 
% 0.72/1.10    uri_rdfs_Literal ) }.
% 0.72/1.10  (22) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_seeAlso, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (26) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_first, 
% 0.72/1.10    uri_rdf_List ) }.
% 0.72/1.10  (27) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_first, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (28) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_rest, 
% 0.72/1.10    uri_rdf_List ) }.
% 0.72/1.10  (14) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_comment, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (106) {G2,W4,D2,L1,V0,M1} R(12,90) { iext( uri_rdf_type, uri_rdfs_domain, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (105) {G2,W4,D2,L1,V0,M1} R(12,91) { iext( uri_rdf_type, uri_rdfs_range, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (104) {G2,W4,D2,L1,V0,M1} R(12,92) { iext( uri_rdf_type, uri_ex_p, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (103) {G2,W4,D2,L1,V0,M1} R(12,94) { iext( uri_rdf_type, 
% 0.72/1.10    uri_rdfs_subClassOf, uri_rdf_Property ) }.
% 0.72/1.10  (13) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_type, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (102) {G1,W2,D2,L1,V0,M1} R(11,2) { ip( uri_rdf_first ) }.
% 0.72/1.10  (101) {G1,W2,D2,L1,V0,M1} R(11,4) { ip( uri_rdf_rest ) }.
% 0.72/1.10  (100) {G1,W2,D2,L1,V0,M1} R(11,5) { ip( uri_rdf__1 ) }.
% 0.72/1.10  (99) {G1,W2,D2,L1,V0,M1} R(11,6) { ip( uri_rdf__2 ) }.
% 0.72/1.10  (12) {G0,W7,D2,L2,V1,M1} I { iext( uri_rdf_type, X, uri_rdf_Property ), ! 
% 0.72/1.10    ip( X ) }.
% 0.72/1.10  (98) {G1,W2,D2,L1,V0,M1} R(11,7) { ip( uri_rdf__3 ) }.
% 0.72/1.10  (97) {G1,W2,D2,L1,V0,M1} R(11,8) { ip( uri_rdf_object ) }.
% 0.72/1.10  (96) {G1,W2,D2,L1,V0,M1} R(11,9) { ip( uri_rdf_value ) }.
% 0.72/1.10  (95) {G1,W2,D2,L1,V0,M1} R(11,10) { ip( uri_rdf_subject ) }.
% 0.72/1.10  (11) {G0,W7,D2,L2,V1,M1} I { ip( X ), ! iext( uri_rdf_type, X, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (29) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_rest, 
% 0.72/1.10    uri_rdf_List ) }.
% 0.72/1.10  (30) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_Alt, 
% 0.72/1.10    uri_rdfs_Container ) }.
% 0.72/1.10  (31) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_Bag, 
% 0.72/1.10    uri_rdfs_Container ) }.
% 0.72/1.10  (33) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty, uri_rdf_Property ) }.
% 0.72/1.10  (10) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_subject, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (34) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_member, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (35) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_member, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (36) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__1, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (37) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__2, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (9) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_value, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (38) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf__3, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (39) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__1, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (40) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__2, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (41) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf__3, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (8) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_object, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (42) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__1, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (43) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__2, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (44) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__3, 
% 0.72/1.10    uri_rdfs_ContainerMembershipProperty ) }.
% 0.72/1.10  (45) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdfs_Seq, 
% 0.72/1.10    uri_rdfs_Container ) }.
% 0.72/1.10  (7) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__3, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (46) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdf_XMLLiteral
% 0.72/1.10    , uri_rdfs_Literal ) }.
% 0.72/1.10  (47) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_XMLLiteral, 
% 0.72/1.10    uri_rdfs_Datatype ) }.
% 0.72/1.10  (94) {G1,W2,D2,L1,V0,M1} R(49,0) { ip( uri_rdfs_subClassOf ) }.
% 0.72/1.10  (49) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_subClassOf, uri_rdfs_Datatype, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (6) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__2, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (50) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_domain, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (52) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_domain, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (58) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_Property, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (59) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_range, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (5) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf__1, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (61) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_range, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (62) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_object, 
% 0.72/1.10    uri_rdfs_Statement ) }.
% 0.72/1.10  (63) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_predicate, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (64) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_predicate, 
% 0.72/1.10    uri_rdfs_Statement ) }.
% 0.72/1.10  (4) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_rest, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (65) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_subject, 
% 0.72/1.10    uri_rdfs_Statement ) }.
% 0.72/1.10  (66) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_subject, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (67) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (71) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_subClassOf, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (3) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_nil, uri_rdf_List )
% 0.72/1.10     }.
% 0.72/1.10  (74) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdfs_subPropertyOf
% 0.72/1.10    , uri_rdf_Property ) }.
% 0.72/1.10  (78) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdfs_subPropertyOf, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (81) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_type, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (93) {G1,W2,D2,L1,V0,M1} R(2,0) { ip( uri_rdf_type ) }.
% 0.72/1.10  (2) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdf_type, uri_rdf_first, 
% 0.72/1.10    uri_rdf_Property ) }.
% 0.72/1.10  (82) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_type, 
% 0.72/1.10    uri_rdfs_Class ) }.
% 0.72/1.10  (92) {G1,W2,D2,L1,V0,M1} R(0,86) { ip( uri_ex_p ) }.
% 0.72/1.10  (91) {G1,W2,D2,L1,V0,M1} R(0,84) { ip( uri_rdfs_range ) }.
% 0.72/1.10  (90) {G1,W2,D2,L1,V0,M1} R(0,83) { ip( uri_rdfs_domain ) }.
% 0.72/1.10  (0) {G0,W7,D2,L2,V3,M1} I { ip( X ), ! iext( X, Y, Z ) }.
% 0.72/1.10  (83) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_domain, uri_rdf_value, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (84) {G0,W4,D2,L1,V0,M1} I { iext( uri_rdfs_range, uri_rdf_value, 
% 0.72/1.10    uri_rdfs_Resource ) }.
% 0.72/1.10  (86) {G0,W4,D2,L1,V0,M1} I { iext( uri_ex_p, uri_ex_s, uri_ex_o ) }.
% 0.72/1.10  (55) {G1,W3,D2,L1,V1,M1} I;r(1) { icext( uri_rdfs_Resource, X ) }.
% 0.72/1.10  (1) {G0,W2,D2,L1,V1,M1} I { ir( X ) }.
% 0.72/1.10  
% 0.72/1.10  
% 0.72/1.10  % SZS output end Saturation
% 0.72/1.10  end of saturation!
% 0.72/1.10  
% 0.72/1.10  Memory use:
% 0.72/1.10  
% 0.72/1.10  space for terms:        4900
% 0.72/1.10  space for clauses:      24573
% 0.72/1.10  
% 0.72/1.10  
% 0.72/1.10  clauses generated:      1301
% 0.72/1.10  clauses kept:           532
% 0.72/1.10  clauses selected:       514
% 0.72/1.10  clauses deleted:        18
% 0.72/1.10  clauses inuse deleted:  0
% 0.72/1.10  
% 0.72/1.10  subsentry:          1884
% 0.72/1.10  literals s-matched: 794
% 0.72/1.10  literals matched:   763
% 0.72/1.10  full subsumption:   6
% 0.72/1.10  
% 0.72/1.10  checksum:           910275077
% 0.72/1.10  
% 0.72/1.10  
% 0.72/1.10  Bliksem ended
%------------------------------------------------------------------------------