%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWB014+3 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n004.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 : 300s
% DateTime : Tue May 5 05:16:49 PM UTC 2026
% Result : Theorem 1.30s 1.60s
% Output : CNFRefutation 1.99s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_172)
% Comments :
%------------------------------------------------------------------------------
fof(testcase_conclusion_fullish_014_Harry_belongs_to_some_Species,conjecture,
? [X21] :
( iext(uri_rdf_type,uri_ex_harry,X21)
& iext(uri_rdf_type,X21,uri_ex_Species) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_conclusion_fullish_014_Harry_belongs_to_some_Species) ).
fof(owl_bool_complementof_class,axiom,
! [X1,X2] :
( iext(uri_owl_complementOf,X1,X2)
=> ( ic(X1)
& ic(X2)
& ! [X3] :
( icext(X1,X3)
<=> ~ icext(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_complementof_class) ).
fof(owl_bool_unionof_class_000,axiom,
! [X1] :
( iext(uri_owl_unionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] : ~ icext(X1,X3) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_000) ).
fof(owl_bool_intersectionof_class_000,axiom,
! [X1] :
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] :
( icext(X1,X3)
<=> ir(X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_000) ).
fof(simple_ir,axiom,
! [X3] : ir(X3),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',simple_ir) ).
fof(owl_parts_ir_def,axiom,
! [X3] :
( ir(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Resource) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ir_def) ).
fof(owl_class_nothing_ext,axiom,
! [X3] : ~ icext(uri_owl_Nothing,X3),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_nothing_ext) ).
fof(rdfs_ir_def,axiom,
! [X3] :
( ir(X3)
<=> icext(uri_rdfs_Resource,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_ir_def) ).
fof(owl_class_thing_ext,axiom,
! [X3] :
( icext(uri_owl_Thing,X3)
<=> ir(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_thing_ext) ).
fof(owl_bool_intersectionof_class_003,axiom,
! [X1,X4,X5,X6,X7,X8,X9] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,X8)
& iext(uri_rdf_first,X8,X9)
& iext(uri_rdf_rest,X8,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ic(X9)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
& icext(X7,X3)
& icext(X9,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_003) ).
fof(owl_bool_unionof_class_003,axiom,
! [X1,X4,X5,X6,X7,X8,X9] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,X8)
& iext(uri_rdf_first,X8,X9)
& iext(uri_rdf_rest,X8,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ic(X9)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
| icext(X7,X3)
| icext(X9,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_003) ).
fof(owl_bool_intersectionof_class_002,axiom,
! [X1,X4,X5,X6,X7] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
& icext(X7,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_002) ).
fof(owl_bool_unionof_class_002,axiom,
! [X1,X4,X5,X6,X7] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
| icext(X7,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_002) ).
fof(owl_restrict_allvaluesfrom,axiom,
! [X1,X11,X2] :
( ( iext(uri_owl_allValuesFrom,X1,X2)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> ! [X10] :
( iext(X11,X3,X10)
=> icext(X2,X10) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_restrict_allvaluesfrom) ).
fof(owl_restrict_somevaluesfrom,axiom,
! [X1,X11,X2] :
( ( iext(uri_owl_someValuesFrom,X1,X2)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> ? [X10] :
( iext(X11,X3,X10)
& icext(X2,X10) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_restrict_somevaluesfrom) ).
fof(owl_bool_unionof_class_001,axiom,
! [X1,X4,X5] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ! [X3] :
( icext(X1,X3)
<=> icext(X5,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_001) ).
fof(owl_bool_intersectionof_class_001,axiom,
! [X1,X4,X5] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ! [X3] :
( icext(X1,X3)
<=> icext(X5,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_001) ).
fof(owl_restrict_hasvalue,axiom,
! [X1,X11,X14] :
( ( iext(uri_owl_hasValue,X1,X14)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> iext(X11,X3,X14) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_restrict_hasvalue) ).
fof(owl_rdfsext_subpropertyof,axiom,
! [X12,X13] :
( iext(uri_rdfs_subPropertyOf,X12,X13)
<=> ( ip(X12)
& ip(X13)
& ! [X3,X10] :
( iext(X12,X3,X10)
=> iext(X13,X3,X10) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_subpropertyof) ).
fof(rdfs_subpropertyof_main,axiom,
! [X11,X17] :
( iext(uri_rdfs_subPropertyOf,X11,X17)
=> ( ip(X11)
& ip(X17)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> iext(X17,X3,X10) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_main) ).
fof(rdfs_subpropertyof_trans,axiom,
! [X11,X17,X18] :
( ( iext(uri_rdfs_subPropertyOf,X11,X17)
& iext(uri_rdfs_subPropertyOf,X17,X18) )
=> iext(uri_rdfs_subPropertyOf,X11,X18) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_trans) ).
fof(rdfs_subclassof_trans,axiom,
! [X2,X15,X16] :
( ( iext(uri_rdfs_subClassOf,X2,X15)
& iext(uri_rdfs_subClassOf,X15,X16) )
=> iext(uri_rdfs_subClassOf,X2,X16) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_trans) ).
fof(rdfs_domain_main,axiom,
! [X11,X2,X3,X10] :
( ( iext(uri_rdfs_domain,X11,X2)
& iext(X11,X3,X10) )
=> icext(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_domain_main) ).
fof(rdfs_range_main,axiom,
! [X11,X2,X3,X10] :
( ( iext(uri_rdfs_range,X11,X2)
& iext(X11,X3,X10) )
=> icext(X2,X10) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_range_main) ).
fof(owl_rdfsext_domain,axiom,
! [X11,X2] :
( iext(uri_rdfs_domain,X11,X2)
<=> ( ip(X11)
& ic(X2)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> icext(X2,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_domain) ).
fof(owl_rdfsext_range,axiom,
! [X11,X2] :
( iext(uri_rdfs_range,X11,X2)
<=> ( ip(X11)
& ip(X2)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> icext(X2,X10) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_range) ).
fof(owl_rdfsext_subclassof,axiom,
! [X5,X7] :
( iext(uri_rdfs_subClassOf,X5,X7)
<=> ( ic(X5)
& ic(X7)
& ! [X3] :
( icext(X5,X3)
=> icext(X7,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_subclassof) ).
fof(rdfs_subclassof_main,axiom,
! [X2,X15] :
( iext(uri_rdfs_subClassOf,X2,X15)
=> ( ic(X2)
& ic(X15)
& ! [X3] :
( icext(X2,X3)
=> icext(X15,X3) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_main) ).
fof(rdfs_cext_def,axiom,
! [X3,X2] :
( iext(uri_rdf_type,X3,X2)
<=> icext(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_cext_def) ).
fof(owl_parts_ioxp_cond_inst,axiom,
! [X3] :
( ioxp(X3)
=> ! [X10,X1] :
( iext(X3,X10,X1)
=> ( ix(X10)
& ix(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_cond_inst) ).
fof(owl_parts_iodp_cond_inst,axiom,
! [X3] :
( iodp(X3)
=> ! [X10,X1] :
( iext(X3,X10,X1)
=> ( ir(X10)
& lv(X1) ) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_cond_inst) ).
fof(owl_prop_unionof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_unionOf,X3,X10)
=> ( ic(X3)
& icext(uri_rdf_List,X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_unionof_ext) ).
fof(owl_prop_intersectionof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_intersectionOf,X3,X10)
=> ( ic(X3)
& icext(uri_rdf_List,X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_intersectionof_ext) ).
fof(owl_prop_somevaluesfrom_ext,axiom,
! [X3,X10] :
( iext(uri_owl_someValuesFrom,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ic(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_somevaluesfrom_ext) ).
fof(owl_prop_onproperty_ext,axiom,
! [X3,X10] :
( iext(uri_owl_onProperty,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ip(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_onproperty_ext) ).
fof(owl_prop_hasvalue_ext,axiom,
! [X3,X10] :
( iext(uri_owl_hasValue,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ir(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_hasvalue_ext) ).
fof(owl_prop_allvaluesfrom_ext,axiom,
! [X3,X10] :
( iext(uri_owl_allValuesFrom,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ic(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_allvaluesfrom_ext) ).
fof(simple_iext_property,axiom,
! [X19,X11,X20] :
( iext(X11,X19,X20)
=> ip(X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',simple_iext_property) ).
fof(owl_prop_complementof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_complementOf,X3,X10)
=> ( ic(X3)
& ic(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_complementof_ext) ).
fof(owl_parts_ix_def,axiom,
! [X3] :
( ix(X3)
<=> iext(uri_rdf_type,X3,uri_owl_Ontology) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ix_def) ).
fof(owl_parts_ioxp_def,axiom,
! [X3] :
( ioxp(X3)
<=> iext(uri_rdf_type,X3,uri_owl_OntologyProperty) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_def) ).
fof(owl_parts_iodp_def,axiom,
! [X3] :
( iodp(X3)
<=> iext(uri_rdf_type,X3,uri_owl_DatatypeProperty) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_def) ).
fof(rdf_type_ip,axiom,
! [X11] :
( iext(uri_rdf_type,X11,uri_rdf_Property)
<=> ip(X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_type_ip) ).
fof(owl_parts_ip_def,axiom,
! [X3] :
( ip(X3)
<=> iext(uri_rdf_type,X3,uri_rdf_Property) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ip_def) ).
fof(owl_parts_ioap_def,axiom,
! [X3] :
( ioap(X3)
<=> iext(uri_rdf_type,X3,uri_owl_AnnotationProperty) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ioap_def) ).
fof(owl_parts_lv_def,axiom,
! [X3] :
( lv(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Literal) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_lv_def) ).
fof(owl_parts_idc_def,axiom,
! [X3] :
( idc(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Datatype) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_def) ).
fof(owl_parts_ic_def,axiom,
! [X3] :
( ic(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ic_def) ).
fof(rdfs_container_containermembershipproperty_instsub_member,axiom,
! [X11] :
( icext(uri_rdfs_ContainerMembershipProperty,X11)
=> iext(uri_rdfs_subPropertyOf,X11,uri_rdfs_member) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_containermembershipproperty_instsub_member) ).
fof(rdfs_datatype_instsub_literal,axiom,
! [X15] :
( icext(uri_rdfs_Datatype,X15)
=> iext(uri_rdfs_subClassOf,X15,uri_rdfs_Literal) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_datatype_instsub_literal) ).
fof(rdfs_subpropertyof_reflex,axiom,
! [X11] :
( ip(X11)
=> iext(uri_rdfs_subPropertyOf,X11,X11) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_reflex) ).
fof(rdfs_subclassof_reflex,axiom,
! [X2] :
( ic(X2)
=> iext(uri_rdfs_subClassOf,X2,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_reflex) ).
fof(rdfs_class_instsub_resource,axiom,
! [X2] :
( ic(X2)
=> iext(uri_rdfs_subClassOf,X2,uri_rdfs_Resource) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_class_instsub_resource) ).
fof(testcase_premise_fullish_014_Harry_belongs_to_some_Species,axiom,
? [X22,X23,X24] :
( iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_harry,X22)
& iext(uri_owl_unionOf,X22,X23)
& iext(uri_rdf_first,X23,uri_ex_Eagle)
& iext(uri_rdf_rest,X23,X24)
& iext(uri_rdf_first,X24,uri_ex_Falcon)
& iext(uri_rdf_rest,X24,uri_rdf_nil) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_premise_fullish_014_Harry_belongs_to_some_Species) ).
fof(owl_parts_idc_cond_inst,axiom,
! [X3] :
( idc(X3)
=> ! [X10] :
( icext(X3,X10)
=> lv(X10) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_cond_inst) ).
fof(rdfs_lv_def,axiom,
! [X3] :
( lv(X3)
<=> icext(uri_rdfs_Literal,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_lv_def) ).
fof(rdfs_ic_def,axiom,
! [X3] :
( ic(X3)
<=> icext(uri_rdfs_Class,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_ic_def) ).
fof(owl_parts_ioxp_cond_set,axiom,
! [X3] :
( ioxp(X3)
=> ip(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_cond_set) ).
fof(owl_parts_iodp_cond_set,axiom,
! [X3] :
( iodp(X3)
=> ip(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_cond_set) ).
fof(owl_parts_ioap_cond_set,axiom,
! [X3] :
( ioap(X3)
=> ip(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ioap_cond_set) ).
fof(owl_parts_idc_cond_set,axiom,
! [X3] :
( idc(X3)
=> ic(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_cond_set) ).
fof(rdfs_annotation_isdefinedby_sub,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_sub) ).
fof(rdfs_dat_xmlliteral_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_dat_xmlliteral_sub) ).
fof(rdfs_container_seq_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_seq_sub) ).
fof(rdfs_container_containermembershipproperty_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_containermembershipproperty_sub) ).
fof(rdfs_container_bag_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_bag_sub) ).
fof(rdfs_container_alt_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_alt_sub) ).
fof(rdfs_datatype_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_datatype_sub) ).
fof(rdfs_reification_predicate_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_predicate_range) ).
fof(rdfs_reification_object_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_object_range) ).
fof(rdfs_container_member_range,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_member_range) ).
fof(rdfs_annotation_label_range,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_label_range) ).
fof(rdfs_annotation_seealso_range,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_seealso_range) ).
fof(rdfs_annotation_isdefinedby_range,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_range) ).
fof(rdfs_annotation_comment_range,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_comment_range) ).
fof(rdfs_reification_subject_range,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_subject_range) ).
fof(rdfs_value_range,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_value_range) ).
fof(rdfs_container_n_range_003,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_003) ).
fof(rdfs_container_n_range_002,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_002) ).
fof(rdfs_container_n_range_001,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_001) ).
fof(rdfs_subpropertyof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_range) ).
fof(rdfs_subclassof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_range) ).
fof(rdfs_range_range,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_range_range) ).
fof(rdfs_domain_range,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_domain_range) ).
fof(rdfs_type_range,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_type_range) ).
fof(rdfs_collection_rest_range,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_collection_rest_range) ).
fof(rdfs_collection_first_range,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_collection_first_range) ).
fof(rdfs_reification_predicate_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_predicate_domain) ).
fof(rdfs_container_member_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_member_domain) ).
fof(rdfs_annotation_label_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_label_domain) ).
fof(rdfs_annotation_seealso_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_seealso_domain) ).
fof(rdfs_annotation_isdefinedby_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_domain) ).
fof(rdfs_annotation_comment_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_comment_domain) ).
fof(rdfs_reification_subject_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_subject_domain) ).
fof(rdfs_value_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_value_domain) ).
fof(rdfs_reification_object_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_reification_object_domain) ).
fof(rdfs_container_n_domain_003,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_003) ).
fof(rdfs_container_n_domain_002,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_002) ).
fof(rdfs_container_n_domain_001,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_001) ).
fof(rdfs_subpropertyof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_domain) ).
fof(rdfs_subclassof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_domain) ).
fof(rdfs_range_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_range_domain) ).
fof(rdfs_domain_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_domain_domain) ).
fof(rdfs_type_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_type_domain) ).
fof(rdfs_collection_rest_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_collection_rest_domain) ).
fof(rdfs_collection_first_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_collection_first_domain) ).
fof(rdfs_dat_xmlliteral_type,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_dat_xmlliteral_type) ).
fof(rdf_reification_subject_type,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_reification_subject_type) ).
fof(rdf_reification_predicate_type,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_reification_predicate_type) ).
fof(rdf_reification_object_type,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_reification_object_type) ).
fof(rdfs_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_003) ).
fof(rdf_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_003) ).
fof(rdfs_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_002) ).
fof(rdf_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_002) ).
fof(rdfs_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_001) ).
fof(rdf_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_001) ).
fof(rdfs_property_type,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_property_type) ).
fof(rdf_value_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_value_type) ).
fof(rdf_type_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_type_type) ).
fof(rdf_collection_rest_type,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_collection_rest_type) ).
fof(rdf_collection_first_type,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_collection_first_type) ).
fof(rdf_collection_nil_type,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_collection_nil_type) ).
fof(owl_prop_somevaluesfrom_type,axiom,
ip(uri_owl_someValuesFrom),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_somevaluesfrom_type) ).
fof(owl_prop_onproperty_type,axiom,
ip(uri_owl_onProperty),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_onproperty_type) ).
fof(owl_prop_hasvalue_type,axiom,
ip(uri_owl_hasValue),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_hasvalue_type) ).
fof(owl_prop_allvaluesfrom_type,axiom,
ip(uri_owl_allValuesFrom),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_allvaluesfrom_type) ).
fof(owl_prop_unionof_type,axiom,
ip(uri_owl_unionOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_unionof_type) ).
fof(owl_prop_intersectionof_type,axiom,
ip(uri_owl_intersectionOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_intersectionof_type) ).
fof(owl_prop_complementof_type,axiom,
ip(uri_owl_complementOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_complementof_type) ).
fof(owl_class_thing_type,axiom,
ic(uri_owl_Thing),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_thing_type) ).
fof(owl_class_nothing_type,axiom,
ic(uri_owl_Nothing),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_nothing_type) ).
fof(i_0_131,negated_conjecture,
~ ? [X21] :
( iext(uri_rdf_type,uri_ex_harry,X21)
& iext(uri_rdf_type,X21,uri_ex_Species) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_014_Harry_belongs_to_some_Species]) ).
fof(i_0_132,plain,
! [X1,X2] :
( iext(uri_owl_complementOf,X1,X2)
=> ( ic(X1)
& ic(X2)
& ! [X3] :
( icext(X1,X3)
<=> ~ icext(X2,X3) ) ) ),
inference(fof_simplification,[status(thm)],[owl_bool_complementof_class]) ).
fof(i_0_133,plain,
! [X1] :
( iext(uri_owl_unionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] : ~ icext(X1,X3) ) ),
inference(fof_simplification,[status(thm)],[owl_bool_unionof_class_000]) ).
fof(i_0_134,plain,
! [X191,X192,X193,X194] :
( ( ic(X191)
| ~ iext(uri_owl_intersectionOf,X191,uri_rdf_nil) )
& ( ~ icext(X191,X192)
| ir(X192)
| ~ iext(uri_owl_intersectionOf,X191,uri_rdf_nil) )
& ( ~ ir(X193)
| icext(X191,X193)
| ~ iext(uri_owl_intersectionOf,X191,uri_rdf_nil) )
& ( ~ icext(X194,esk1_1(X194))
| ~ ir(esk1_1(X194))
| ~ ic(X194)
| iext(uri_owl_intersectionOf,X194,uri_rdf_nil) )
& ( icext(X194,esk1_1(X194))
| ir(esk1_1(X194))
| ~ ic(X194)
| iext(uri_owl_intersectionOf,X194,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_000])])])])])]) ).
fof(i_0_135,plain,
! [X381] : ir(X381),
inference(variable_rename,[status(thm)],[simple_ir]) ).
fof(i_0_136,plain,
! [X279] :
( ( ~ ir(X279)
| iext(uri_rdf_type,X279,uri_rdfs_Resource) )
& ( ~ iext(uri_rdf_type,X279,uri_rdfs_Resource)
| ir(X279) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ir_def])]) ).
fof(i_0_137,plain,
! [X3] : ~ icext(uri_owl_Nothing,X3),
inference(fof_simplification,[status(thm)],[owl_class_nothing_ext]) ).
fof(i_0_138,plain,
! [X357] :
( ( ~ ir(X357)
| icext(uri_rdfs_Resource,X357) )
& ( ~ icext(uri_rdfs_Resource,X357)
| ir(X357) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ir_def])]) ).
fof(i_0_139,plain,
! [X249] :
( ( ~ icext(uri_owl_Thing,X249)
| ir(X249) )
& ( ~ ir(X249)
| icext(uri_owl_Thing,X249) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_class_thing_ext])]) ).
fof(i_0_140,plain,
! [X210,X211,X212,X213,X214,X215,X216,X217,X218] :
( ( ic(X210)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( ic(X212)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( ic(X214)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( ic(X216)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X212,X217)
| ~ icext(X210,X217)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X214,X217)
| ~ icext(X210,X217)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X216,X217)
| ~ icext(X210,X217)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( ~ icext(X212,X218)
| ~ icext(X214,X218)
| ~ icext(X216,X218)
| icext(X210,X218)
| ~ iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( ~ icext(X210,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ icext(X212,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ icext(X214,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ icext(X216,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| ~ ic(X216)
| iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X212,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| icext(X210,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| ~ ic(X216)
| iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X214,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| icext(X210,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| ~ ic(X216)
| iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) )
& ( icext(X216,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| icext(X210,esk4_7(X210,X211,X212,X213,X214,X215,X216))
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| ~ ic(X216)
| iext(uri_owl_intersectionOf,X210,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,X215)
| ~ iext(uri_rdf_first,X215,X216)
| ~ iext(uri_rdf_rest,X215,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_003])])])])])]) ).
fof(i_0_141,plain,
! [X238,X239,X240,X241,X242,X243,X244,X245,X246] :
( ( ic(X238)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ic(X240)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ic(X242)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ic(X244)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X238,X245)
| icext(X240,X245)
| icext(X242,X245)
| icext(X244,X245)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X240,X246)
| icext(X238,X246)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X242,X246)
| icext(X238,X246)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X244,X246)
| icext(X238,X246)
| ~ iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X240,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ icext(X238,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| ~ ic(X244)
| iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X242,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ icext(X238,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| ~ ic(X244)
| iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( ~ icext(X244,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ icext(X238,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| ~ ic(X244)
| iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) )
& ( icext(X238,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| icext(X240,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| icext(X242,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| icext(X244,esk8_7(X238,X239,X240,X241,X242,X243,X244))
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| ~ ic(X244)
| iext(uri_owl_unionOf,X238,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,X243)
| ~ iext(uri_rdf_first,X243,X244)
| ~ iext(uri_rdf_rest,X243,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_003])])])])])]) ).
fof(i_0_142,plain,
! [X202,X203,X204,X205,X206,X207,X208] :
( ( ic(X202)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( ic(X204)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( ic(X206)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( icext(X204,X207)
| ~ icext(X202,X207)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( icext(X206,X207)
| ~ icext(X202,X207)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( ~ icext(X204,X208)
| ~ icext(X206,X208)
| icext(X202,X208)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( ~ icext(X202,esk3_5(X202,X203,X204,X205,X206))
| ~ icext(X204,esk3_5(X202,X203,X204,X205,X206))
| ~ icext(X206,esk3_5(X202,X203,X204,X205,X206))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( icext(X204,esk3_5(X202,X203,X204,X205,X206))
| icext(X202,esk3_5(X202,X203,X204,X205,X206))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) )
& ( icext(X206,esk3_5(X202,X203,X204,X205,X206))
| icext(X202,esk3_5(X202,X203,X204,X205,X206))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_002])])])])])]) ).
fof(i_0_143,plain,
! [X230,X231,X232,X233,X234,X235,X236] :
( ( ic(X230)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ic(X232)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ic(X234)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ~ icext(X230,X235)
| icext(X232,X235)
| icext(X234,X235)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ~ icext(X232,X236)
| icext(X230,X236)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ~ icext(X234,X236)
| icext(X230,X236)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ~ icext(X232,esk7_5(X230,X231,X232,X233,X234))
| ~ icext(X230,esk7_5(X230,X231,X232,X233,X234))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( ~ icext(X234,esk7_5(X230,X231,X232,X233,X234))
| ~ icext(X230,esk7_5(X230,X231,X232,X233,X234))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) )
& ( icext(X230,esk7_5(X230,X231,X232,X233,X234))
| icext(X232,esk7_5(X230,X231,X232,X233,X234))
| icext(X234,esk7_5(X230,X231,X232,X233,X234))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_002])])])])])]) ).
fof(i_0_144,plain,
! [X328,X329,X330,X331,X332,X333] :
( ( ~ icext(X328,X331)
| ~ iext(X329,X331,X332)
| icext(X330,X332)
| ~ iext(uri_owl_allValuesFrom,X328,X330)
| ~ iext(uri_owl_onProperty,X328,X329) )
& ( iext(X329,X333,esk17_4(X328,X329,X330,X333))
| icext(X328,X333)
| ~ iext(uri_owl_allValuesFrom,X328,X330)
| ~ iext(uri_owl_onProperty,X328,X329) )
& ( ~ icext(X330,esk17_4(X328,X329,X330,X333))
| icext(X328,X333)
| ~ iext(uri_owl_allValuesFrom,X328,X330)
| ~ iext(uri_owl_onProperty,X328,X329) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_allvaluesfrom])])])])])]) ).
fof(i_0_145,plain,
! [X339,X340,X341,X342,X344,X345] :
( ( iext(X340,X342,esk18_4(X339,X340,X341,X342))
| ~ icext(X339,X342)
| ~ iext(uri_owl_someValuesFrom,X339,X341)
| ~ iext(uri_owl_onProperty,X339,X340) )
& ( icext(X341,esk18_4(X339,X340,X341,X342))
| ~ icext(X339,X342)
| ~ iext(uri_owl_someValuesFrom,X339,X341)
| ~ iext(uri_owl_onProperty,X339,X340) )
& ( ~ iext(X340,X344,X345)
| ~ icext(X341,X345)
| icext(X339,X344)
| ~ iext(uri_owl_someValuesFrom,X339,X341)
| ~ iext(uri_owl_onProperty,X339,X340) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_somevaluesfrom])])])])])]) ).
fof(i_0_146,plain,
! [X224,X225,X226,X227,X228] :
( ( ic(X224)
| ~ iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ic(X226)
| ~ iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X224,X227)
| icext(X226,X227)
| ~ iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X226,X228)
| icext(X224,X228)
| ~ iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X224,esk6_3(X224,X225,X226))
| ~ icext(X226,esk6_3(X224,X225,X226))
| ~ ic(X224)
| ~ ic(X226)
| iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( icext(X224,esk6_3(X224,X225,X226))
| icext(X226,esk6_3(X224,X225,X226))
| ~ ic(X224)
| ~ ic(X226)
| iext(uri_owl_unionOf,X224,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_001])])])])])]) ).
fof(i_0_147,plain,
! [X196,X197,X198,X199,X200] :
( ( ic(X196)
| ~ iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ic(X198)
| ~ iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ~ icext(X196,X199)
| icext(X198,X199)
| ~ iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ~ icext(X198,X200)
| icext(X196,X200)
| ~ iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ~ icext(X196,esk2_3(X196,X197,X198))
| ~ icext(X198,esk2_3(X196,X197,X198))
| ~ ic(X196)
| ~ ic(X198)
| iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( icext(X196,esk2_3(X196,X197,X198))
| icext(X198,esk2_3(X196,X197,X198))
| ~ ic(X196)
| ~ ic(X198)
| iext(uri_owl_intersectionOf,X196,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_001])])])])])]) ).
fof(i_0_148,plain,
! [X335,X336,X337,X338] :
( ( ~ icext(X335,X338)
| iext(X336,X338,X337)
| ~ iext(uri_owl_hasValue,X335,X337)
| ~ iext(uri_owl_onProperty,X335,X336) )
& ( ~ iext(X336,X338,X337)
| icext(X335,X338)
| ~ iext(uri_owl_hasValue,X335,X337)
| ~ iext(uri_owl_onProperty,X335,X336) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_hasvalue])])])]) ).
fof(i_0_149,plain,
! [X320,X321,X322,X323,X324,X325] :
( ( ip(X320)
| ~ iext(uri_rdfs_subPropertyOf,X320,X321) )
& ( ip(X321)
| ~ iext(uri_rdfs_subPropertyOf,X320,X321) )
& ( ~ iext(X320,X322,X323)
| iext(X321,X322,X323)
| ~ iext(uri_rdfs_subPropertyOf,X320,X321) )
& ( iext(X324,esk15_2(X324,X325),esk16_2(X324,X325))
| ~ ip(X324)
| ~ ip(X325)
| iext(uri_rdfs_subPropertyOf,X324,X325) )
& ( ~ iext(X325,esk15_2(X324,X325),esk16_2(X324,X325))
| ~ ip(X324)
| ~ ip(X325)
| iext(uri_rdfs_subPropertyOf,X324,X325) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_subpropertyof])])])])])]) ).
fof(i_0_150,plain,
! [X370,X371,X372,X373] :
( ( ip(X370)
| ~ iext(uri_rdfs_subPropertyOf,X370,X371) )
& ( ip(X371)
| ~ iext(uri_rdfs_subPropertyOf,X370,X371) )
& ( ~ iext(X370,X372,X373)
| iext(X371,X372,X373)
| ~ iext(uri_rdfs_subPropertyOf,X370,X371) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])])])]) ).
fof(i_0_151,plain,
! [X375,X376,X377] :
( ~ iext(uri_rdfs_subPropertyOf,X375,X376)
| ~ iext(uri_rdfs_subPropertyOf,X376,X377)
| iext(uri_rdfs_subPropertyOf,X375,X377) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])]) ).
fof(i_0_152,plain,
! [X367,X368,X369] :
( ~ iext(uri_rdfs_subClassOf,X367,X368)
| ~ iext(uri_rdfs_subClassOf,X368,X369)
| iext(uri_rdfs_subClassOf,X367,X369) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])]) ).
fof(i_0_153,plain,
! [X352,X353,X354,X355] :
( ~ iext(uri_rdfs_domain,X352,X353)
| ~ iext(X352,X354,X355)
| icext(X353,X354) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_domain_main])]) ).
fof(i_0_154,plain,
! [X359,X360,X361,X362] :
( ~ iext(uri_rdfs_range,X359,X360)
| ~ iext(X359,X361,X362)
| icext(X360,X362) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_range_main])]) ).
fof(i_0_155,plain,
! [X298,X299,X300,X301,X302,X303] :
( ( ip(X298)
| ~ iext(uri_rdfs_domain,X298,X299) )
& ( ic(X299)
| ~ iext(uri_rdfs_domain,X298,X299) )
& ( ~ iext(X298,X300,X301)
| icext(X299,X300)
| ~ iext(uri_rdfs_domain,X298,X299) )
& ( iext(X302,esk10_2(X302,X303),esk11_2(X302,X303))
| ~ ip(X302)
| ~ ic(X303)
| iext(uri_rdfs_domain,X302,X303) )
& ( ~ icext(X303,esk10_2(X302,X303))
| ~ ip(X302)
| ~ ic(X303)
| iext(uri_rdfs_domain,X302,X303) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_domain])])])])])]) ).
fof(i_0_156,plain,
! [X306,X307,X308,X309,X310,X311] :
( ( ip(X306)
| ~ iext(uri_rdfs_range,X306,X307) )
& ( ip(X307)
| ~ iext(uri_rdfs_range,X306,X307) )
& ( ~ iext(X306,X308,X309)
| icext(X307,X309)
| ~ iext(uri_rdfs_range,X306,X307) )
& ( iext(X310,esk12_2(X310,X311),esk13_2(X310,X311))
| ~ ip(X310)
| ~ ip(X311)
| iext(uri_rdfs_range,X310,X311) )
& ( ~ icext(X311,esk13_2(X310,X311))
| ~ ip(X310)
| ~ ip(X311)
| iext(uri_rdfs_range,X310,X311) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_range])])])])])]) ).
fof(i_0_157,negated_conjecture,
! [X383] :
( ~ iext(uri_rdf_type,uri_ex_harry,X383)
| ~ iext(uri_rdf_type,X383,uri_ex_Species) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_131])]) ).
fof(i_0_158,plain,
! [X314,X315,X316,X317,X318] :
( ( ic(X314)
| ~ iext(uri_rdfs_subClassOf,X314,X315) )
& ( ic(X315)
| ~ iext(uri_rdfs_subClassOf,X314,X315) )
& ( ~ icext(X314,X316)
| icext(X315,X316)
| ~ iext(uri_rdfs_subClassOf,X314,X315) )
& ( icext(X317,esk14_2(X317,X318))
| ~ ic(X317)
| ~ ic(X318)
| iext(uri_rdfs_subClassOf,X317,X318) )
& ( ~ icext(X318,esk14_2(X317,X318))
| ~ ic(X317)
| ~ ic(X318)
| iext(uri_rdfs_subClassOf,X317,X318) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof])])])])])]) ).
fof(i_0_159,plain,
! [X188,X189,X190] :
( ( ic(X188)
| ~ iext(uri_owl_complementOf,X188,X189) )
& ( ic(X189)
| ~ iext(uri_owl_complementOf,X188,X189) )
& ( ~ icext(X188,X190)
| ~ icext(X189,X190)
| ~ iext(uri_owl_complementOf,X188,X189) )
& ( icext(X189,X190)
| icext(X188,X190)
| ~ iext(uri_owl_complementOf,X188,X189) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_132])])])]) ).
fof(i_0_160,plain,
! [X363,X364,X365] :
( ( ic(X363)
| ~ iext(uri_rdfs_subClassOf,X363,X364) )
& ( ic(X364)
| ~ iext(uri_rdfs_subClassOf,X363,X364) )
& ( ~ icext(X363,X365)
| icext(X364,X365)
| ~ iext(uri_rdfs_subClassOf,X363,X364) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])])])]) ).
fof(i_0_161,plain,
! [X220,X221,X222] :
( ( ic(X220)
| ~ iext(uri_owl_unionOf,X220,uri_rdf_nil) )
& ( ~ icext(X220,X221)
| ~ iext(uri_owl_unionOf,X220,uri_rdf_nil) )
& ( ~ ic(X222)
| icext(X222,esk5_1(X222))
| iext(uri_owl_unionOf,X222,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_133])])])])])]) ).
fof(i_0_162,plain,
! [X347,X348] :
( ( ~ iext(uri_rdf_type,X347,X348)
| icext(X348,X347) )
& ( ~ icext(X348,X347)
| iext(uri_rdf_type,X347,X348) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_cext_def])]) ).
fof(i_0_163,plain,
! [X268,X269,X270] :
( ( ix(X269)
| ~ iext(X268,X269,X270)
| ~ ioxp(X268) )
& ( ix(X270)
| ~ iext(X268,X269,X270)
| ~ ioxp(X268) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_inst])])])]) ).
fof(i_0_164,plain,
! [X263,X264,X265] :
( ( ir(X264)
| ~ iext(X263,X264,X265)
| ~ iodp(X263) )
& ( lv(X265)
| ~ iext(X263,X264,X265)
| ~ iodp(X263) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_inst])])])]) ).
fof(i_0_165,plain,
! [X296,X297] :
( ( ic(X296)
| ~ iext(uri_owl_unionOf,X296,X297) )
& ( icext(uri_rdf_List,X297)
| ~ iext(uri_owl_unionOf,X296,X297) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_unionof_ext])])]) ).
fof(i_0_166,plain,
! [X290,X291] :
( ( ic(X290)
| ~ iext(uri_owl_intersectionOf,X290,X291) )
& ( icext(uri_rdf_List,X291)
| ~ iext(uri_owl_intersectionOf,X290,X291) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_intersectionof_ext])])]) ).
fof(i_0_167,plain,
! [X294,X295] :
( ( icext(uri_owl_Restriction,X294)
| ~ iext(uri_owl_someValuesFrom,X294,X295) )
& ( ic(X295)
| ~ iext(uri_owl_someValuesFrom,X294,X295) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_somevaluesfrom_ext])])]) ).
fof(i_0_168,plain,
! [X292,X293] :
( ( icext(uri_owl_Restriction,X292)
| ~ iext(uri_owl_onProperty,X292,X293) )
& ( ip(X293)
| ~ iext(uri_owl_onProperty,X292,X293) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_onproperty_ext])])]) ).
fof(i_0_169,plain,
! [X288,X289] :
( ( icext(uri_owl_Restriction,X288)
| ~ iext(uri_owl_hasValue,X288,X289) )
& ( ir(X289)
| ~ iext(uri_owl_hasValue,X288,X289) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_hasvalue_ext])])]) ).
fof(i_0_170,plain,
! [X284,X285] :
( ( icext(uri_owl_Restriction,X284)
| ~ iext(uri_owl_allValuesFrom,X284,X285) )
& ( ic(X285)
| ~ iext(uri_owl_allValuesFrom,X284,X285) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_allvaluesfrom_ext])])]) ).
cnf(i_0_171,plain,
( icext(X2,X1)
| ~ ir(X1)
| ~ iext(uri_owl_intersectionOf,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_134]) ).
cnf(i_0_172,plain,
ir(X1),
inference(split_conjunct,[status(thm)],[i_0_135]) ).
cnf(i_0_173,plain,
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
| ~ icext(X1,esk1_1(X1))
| ~ ir(esk1_1(X1))
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]) ).
fof(i_0_174,plain,
! [X378,X379,X380] :
( ~ iext(X379,X378,X380)
| ip(X379) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[simple_iext_property])]) ).
fof(i_0_175,plain,
! [X286,X287] :
( ( ic(X286)
| ~ iext(uri_owl_complementOf,X286,X287) )
& ( ic(X287)
| ~ iext(uri_owl_complementOf,X286,X287) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_complementof_ext])])]) ).
fof(i_0_176,plain,
! [X281] :
( ( ~ ix(X281)
| iext(uri_rdf_type,X281,uri_owl_Ontology) )
& ( ~ iext(uri_rdf_type,X281,uri_owl_Ontology)
| ix(X281) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ix_def])]) ).
fof(i_0_177,plain,
! [X272] :
( ( ~ ioxp(X272)
| iext(uri_rdf_type,X272,uri_owl_OntologyProperty) )
& ( ~ iext(uri_rdf_type,X272,uri_owl_OntologyProperty)
| ioxp(X272) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_def])]) ).
fof(i_0_178,plain,
! [X267] :
( ( ~ iodp(X267)
| iext(uri_rdf_type,X267,uri_owl_DatatypeProperty) )
& ( ~ iext(uri_rdf_type,X267,uri_owl_DatatypeProperty)
| iodp(X267) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_def])]) ).
fof(i_0_179,plain,
! [X346] :
( ( ~ iext(uri_rdf_type,X346,uri_rdf_Property)
| ip(X346) )
& ( ~ ip(X346)
| iext(uri_rdf_type,X346,uri_rdf_Property) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdf_type_ip])]) ).
fof(i_0_180,plain,
! [X277] :
( ( ~ ip(X277)
| iext(uri_rdf_type,X277,uri_rdf_Property) )
& ( ~ iext(uri_rdf_type,X277,uri_rdf_Property)
| ip(X277) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ip_def])]) ).
fof(i_0_181,plain,
! [X262] :
( ( ~ ioap(X262)
| iext(uri_rdf_type,X262,uri_owl_AnnotationProperty) )
& ( ~ iext(uri_rdf_type,X262,uri_owl_AnnotationProperty)
| ioap(X262) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_def])]) ).
fof(i_0_182,plain,
! [X283] :
( ( ~ lv(X283)
| iext(uri_rdf_type,X283,uri_rdfs_Literal) )
& ( ~ iext(uri_rdf_type,X283,uri_rdfs_Literal)
| lv(X283) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_lv_def])]) ).
fof(i_0_183,plain,
! [X257] :
( ( ~ idc(X257)
| iext(uri_rdf_type,X257,uri_rdfs_Datatype) )
& ( ~ iext(uri_rdf_type,X257,uri_rdfs_Datatype)
| idc(X257) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_def])]) ).
fof(i_0_184,plain,
! [X253] :
( ( ~ ic(X253)
| iext(uri_rdf_type,X253,uri_rdfs_Class) )
& ( ~ iext(uri_rdf_type,X253,uri_rdfs_Class)
| ic(X253) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ic_def])]) ).
fof(i_0_185,plain,
! [X350] :
( ~ icext(uri_rdfs_ContainerMembershipProperty,X350)
| iext(uri_rdfs_subPropertyOf,X350,uri_rdfs_member) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])]) ).
fof(i_0_186,plain,
! [X351] :
( ~ icext(uri_rdfs_Datatype,X351)
| iext(uri_rdfs_subClassOf,X351,uri_rdfs_Literal) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])]) ).
fof(i_0_187,plain,
! [X374] :
( ~ ip(X374)
| iext(uri_rdfs_subPropertyOf,X374,X374) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])]) ).
fof(i_0_188,plain,
! [X366] :
( ~ ic(X366)
| iext(uri_rdfs_subClassOf,X366,X366) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])]) ).
fof(i_0_189,plain,
! [X349] :
( ~ ic(X349)
| iext(uri_rdfs_subClassOf,X349,uri_rdfs_Resource) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])]) ).
cnf(i_0_190,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Resource)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]) ).
fof(i_0_191,plain,
( iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)
& iext(uri_rdf_type,uri_ex_harry,esk19_0)
& iext(uri_owl_unionOf,esk19_0,esk20_0)
& iext(uri_rdf_first,esk20_0,uri_ex_Eagle)
& iext(uri_rdf_rest,esk20_0,esk21_0)
& iext(uri_rdf_first,esk21_0,uri_ex_Falcon)
& iext(uri_rdf_rest,esk21_0,uri_rdf_nil) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[testcase_premise_fullish_014_Harry_belongs_to_some_Species])]) ).
fof(i_0_192,plain,
! [X254,X255] :
( ~ idc(X254)
| ~ icext(X254,X255)
| lv(X255) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_inst])])]) ).
fof(i_0_193,plain,
! [X358] :
( ( ~ lv(X358)
| icext(uri_rdfs_Literal,X358) )
& ( ~ icext(uri_rdfs_Literal,X358)
| lv(X358) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_lv_def])]) ).
fof(i_0_194,plain,
! [X356] :
( ( ~ ic(X356)
| icext(uri_rdfs_Class,X356) )
& ( ~ icext(uri_rdfs_Class,X356)
| ic(X356) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ic_def])]) ).
fof(i_0_195,plain,
! [X248] : ~ icext(uri_owl_Nothing,X248),
inference(variable_rename,[status(thm)],[i_0_137]) ).
cnf(i_0_196,plain,
( icext(uri_rdfs_Resource,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_138]) ).
cnf(i_0_197,plain,
( icext(uri_owl_Thing,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_139]) ).
fof(i_0_198,plain,
! [X271] :
( ~ ioxp(X271)
| ip(X271) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_set])]) ).
fof(i_0_199,plain,
! [X266] :
( ~ iodp(X266)
| ip(X266) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_set])]) ).
fof(i_0_200,plain,
! [X261] :
( ~ ioap(X261)
| ip(X261) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_cond_set])]) ).
fof(i_0_201,plain,
! [X256] :
( ~ idc(X256)
| ic(X256) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set])]) ).
cnf(i_0_202,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X3,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X5,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X7,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_203,plain,
( icext(X1,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X3,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X5,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X7,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_204,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X4,X5,X6,X7,X1))
| ~ icext(X2,esk8_7(X2,X3,X4,X5,X6,X7,X1))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X6)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_205,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X4,X5,X1,X6,X7))
| ~ icext(X2,esk8_7(X2,X3,X4,X5,X1,X6,X7))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_206,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X1,X4,X5,X6,X7))
| ~ icext(X2,esk8_7(X2,X3,X1,X4,X5,X6,X7))
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_207,plain,
( icext(X1,esk4_7(X2,X3,X1,X4,X5,X6,X7))
| icext(X2,esk4_7(X2,X3,X1,X4,X5,X6,X7))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_208,plain,
( icext(X1,esk4_7(X2,X3,X4,X5,X1,X6,X7))
| icext(X2,esk4_7(X2,X3,X4,X5,X1,X6,X7))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_209,plain,
( icext(X1,esk4_7(X2,X3,X4,X5,X6,X7,X1))
| icext(X2,esk4_7(X2,X3,X4,X5,X6,X7,X1))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X6)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_210,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk3_5(X1,X2,X3,X4,X5))
| ~ icext(X3,esk3_5(X1,X2,X3,X4,X5))
| ~ icext(X5,esk3_5(X1,X2,X3,X4,X5))
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_211,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk7_5(X2,X3,X4,X5,X1))
| ~ icext(X2,esk7_5(X2,X3,X4,X5,X1))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_212,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk7_5(X2,X3,X1,X4,X5))
| ~ icext(X2,esk7_5(X2,X3,X1,X4,X5))
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_213,plain,
( icext(X1,esk7_5(X1,X2,X3,X4,X5))
| icext(X3,esk7_5(X1,X2,X3,X4,X5))
| icext(X5,esk7_5(X1,X2,X3,X4,X5))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_214,plain,
( icext(X1,esk3_5(X2,X3,X1,X4,X5))
| icext(X2,esk3_5(X2,X3,X1,X4,X5))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_215,plain,
( icext(X1,esk3_5(X2,X3,X4,X5,X1))
| icext(X2,esk3_5(X2,X3,X4,X5,X1))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_216,plain,
( icext(X2,X4)
| ~ icext(X1,esk17_4(X2,X3,X1,X4))
| ~ iext(uri_owl_allValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_217,plain,
( iext(X1,X2,esk18_4(X3,X1,X4,X2))
| ~ icext(X3,X2)
| ~ iext(uri_owl_someValuesFrom,X3,X4)
| ~ iext(uri_owl_onProperty,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_218,plain,
( iext(X1,X2,esk17_4(X3,X1,X4,X2))
| icext(X3,X2)
| ~ iext(uri_owl_allValuesFrom,X3,X4)
| ~ iext(uri_owl_onProperty,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_219,plain,
( icext(X1,esk18_4(X2,X3,X1,X4))
| ~ icext(X2,X4)
| ~ iext(uri_owl_someValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_220,plain,
( icext(X5,X2)
| ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ icext(X4,X2)
| ~ iext(uri_owl_intersectionOf,X5,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X3)
| ~ iext(uri_rdf_rest,X7,X8)
| ~ iext(uri_rdf_first,X8,X4)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_221,plain,
( icext(X3,X2)
| icext(X4,X2)
| icext(X5,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X6)
| ~ iext(uri_rdf_first,X6,X3)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X4)
| ~ iext(uri_rdf_rest,X7,X8)
| ~ iext(uri_rdf_first,X8,X5)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_222,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_223,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_224,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,X8)
| ~ iext(uri_rdf_first,X8,X1)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_225,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_226,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_227,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,X8)
| ~ iext(uri_rdf_first,X8,X1)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_228,plain,
( iext(uri_owl_unionOf,X1,X2)
| ~ icext(X1,esk6_3(X1,X2,X3))
| ~ icext(X3,esk6_3(X1,X2,X3))
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_229,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk2_3(X1,X2,X3))
| ~ icext(X3,esk2_3(X1,X2,X3))
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_230,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_231,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_232,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_233,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_234,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_235,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_236,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_237,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_238,plain,
( icext(X4,X2)
| ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X4,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X3)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_239,plain,
( icext(X1,esk6_3(X1,X2,X3))
| icext(X3,esk6_3(X1,X2,X3))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_240,plain,
( icext(X1,esk2_3(X1,X2,X3))
| icext(X3,esk2_3(X1,X2,X3))
| iext(uri_owl_intersectionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_241,plain,
( icext(X3,X2)
| icext(X4,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X5)
| ~ iext(uri_rdf_first,X5,X3)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X4)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_242,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_243,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_244,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_245,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_246,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_247,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_248,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_249,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_250,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_251,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_252,plain,
( icext(X5,X2)
| ~ iext(X1,X2,X3)
| ~ icext(X4,X3)
| ~ iext(uri_owl_someValuesFrom,X5,X4)
| ~ iext(uri_owl_onProperty,X5,X1) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_253,plain,
( icext(X5,X4)
| ~ icext(X1,X2)
| ~ iext(X3,X2,X4)
| ~ iext(uri_owl_allValuesFrom,X1,X5)
| ~ iext(uri_owl_onProperty,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_254,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_255,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X4)
| ~ iext(uri_rdf_first,X4,X3)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_256,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,X4)
| ~ iext(uri_rdf_first,X4,X3)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_257,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_258,plain,
( icext(X4,X2)
| ~ iext(X1,X2,X3)
| ~ iext(uri_owl_hasValue,X4,X3)
| ~ iext(uri_owl_onProperty,X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_259,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_260,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_261,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_262,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_263,plain,
( iext(X3,X2,X4)
| ~ icext(X1,X2)
| ~ iext(uri_owl_hasValue,X1,X4)
| ~ iext(uri_owl_onProperty,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_264,plain,
( iext(uri_rdfs_subPropertyOf,X2,X1)
| ~ iext(X1,esk15_2(X2,X1),esk16_2(X2,X1))
| ~ ip(X2)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_265,plain,
( iext(X4,X2,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_266,plain,
( iext(X4,X2,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_267,plain,
( iext(uri_rdfs_subPropertyOf,X1,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| ~ iext(uri_rdfs_subPropertyOf,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_268,plain,
( iext(uri_rdfs_subClassOf,X1,X3)
| ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_269,plain,
( icext(X2,X3)
| ~ iext(uri_rdfs_domain,X1,X2)
| ~ iext(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_270,plain,
( icext(X2,X4)
| ~ iext(uri_rdfs_range,X1,X2)
| ~ iext(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_154]),
[final] ).
cnf(i_0_271,plain,
( icext(X4,X2)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_domain,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_272,plain,
( icext(X4,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_range,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_273,plain,
( iext(X1,esk15_2(X1,X2),esk16_2(X1,X2))
| iext(uri_rdfs_subPropertyOf,X1,X2)
| ~ ip(X1)
| ~ ip(X2) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_274,plain,
( iext(X1,esk12_2(X1,X2),esk13_2(X1,X2))
| iext(uri_rdfs_range,X1,X2)
| ~ ip(X1)
| ~ ip(X2) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_275,plain,
( iext(X1,esk10_2(X1,X2),esk11_2(X1,X2))
| iext(uri_rdfs_domain,X1,X2)
| ~ ip(X1)
| ~ ic(X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_276,negated_conjecture,
( ~ iext(uri_rdf_type,uri_ex_harry,X1)
| ~ iext(uri_rdf_type,X1,uri_ex_Species) ),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_277,plain,
( iext(uri_rdfs_subClassOf,X2,X1)
| ~ icext(X1,esk14_2(X2,X1))
| ~ ic(X2)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_278,plain,
( iext(uri_rdfs_range,X2,X1)
| ~ icext(X1,esk13_2(X2,X1))
| ~ ip(X2)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_279,plain,
( iext(uri_rdfs_domain,X2,X1)
| ~ icext(X1,esk10_2(X2,X1))
| ~ ip(X2)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_280,plain,
( ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_complementOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_281,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_rdfs_subClassOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_282,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_rdfs_subClassOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_283,plain,
( icext(X1,X2)
| icext(X3,X2)
| ~ iext(uri_owl_complementOf,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_284,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_285,plain,
( ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_286,plain,
( icext(X2,X1)
| ~ iext(uri_rdf_type,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_287,plain,
( ix(X1)
| ~ iext(X2,X1,X3)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_288,plain,
( ix(X1)
| ~ iext(X2,X3,X1)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_289,plain,
( lv(X1)
| ~ iext(X2,X3,X1)
| ~ iodp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_164]),
[final] ).
cnf(i_0_290,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_unionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_291,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_intersectionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_292,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_someValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_293,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_onProperty,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_294,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_hasValue,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_169]),
[final] ).
cnf(i_0_295,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_allValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_296,plain,
( icext(X2,X1)
| ~ iext(uri_owl_intersectionOf,X2,uri_rdf_nil) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_171,c_0_172])]),
[final] ).
cnf(i_0_297,plain,
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
| ~ ic(X1)
| ~ icext(X1,esk1_1(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_173,c_0_172])]),
[final] ).
cnf(i_0_298,plain,
( ip(X1)
| ~ iext(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_174]),
[final] ).
cnf(i_0_299,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_300,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_301,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_302,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_303,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_304,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_305,plain,
( ip(X1)
| ~ iext(uri_rdfs_domain,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_306,plain,
( ip(X1)
| ~ iext(uri_owl_onProperty,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_307,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_308,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_309,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_310,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_311,plain,
( ic(X1)
| ~ iext(uri_rdfs_domain,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_312,plain,
( ic(X1)
| ~ iext(uri_owl_someValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_313,plain,
( ic(X1)
| ~ iext(uri_owl_allValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_314,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_315,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_316,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_317,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_318,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_319,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_320,plain,
( ix(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_Ontology) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_321,plain,
( ioxp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_OntologyProperty) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_322,plain,
( iodp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_DatatypeProperty) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_323,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_324,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_325,plain,
( ioap(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_AnnotationProperty) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_326,plain,
( lv(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Literal) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_327,plain,
( idc(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Datatype) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_328,plain,
( ic(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Class) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_329,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_330,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_331,plain,
( icext(X1,esk5_1(X1))
| iext(uri_owl_unionOf,X1,uri_rdf_nil)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_332,plain,
( iext(uri_rdf_type,X2,X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_333,plain,
( iext(uri_rdfs_subPropertyOf,X1,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,X1) ),
inference(split_conjunct,[status(thm)],[i_0_185]),
[final] ).
cnf(i_0_334,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,X1) ),
inference(split_conjunct,[status(thm)],[i_0_186]),
[final] ).
cnf(i_0_335,plain,
( iext(uri_rdfs_subPropertyOf,X1,X1)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_187]),
[final] ).
cnf(i_0_336,plain,
( iext(uri_rdfs_subClassOf,X1,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_188]),
[final] ).
cnf(i_0_337,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Resource)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_189]),
[final] ).
cnf(i_0_338,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Literal)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_339,plain,
( iext(uri_rdf_type,X1,uri_owl_Ontology)
| ~ ix(X1) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_340,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_341,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_342,plain,
( iext(uri_rdf_type,X1,uri_owl_OntologyProperty)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_343,plain,
( iext(uri_rdf_type,X1,uri_owl_DatatypeProperty)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_344,plain,
( iext(uri_rdf_type,X1,uri_owl_AnnotationProperty)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_345,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Datatype)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_346,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Class)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_347,plain,
iext(uri_rdf_type,X1,uri_rdfs_Resource),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_190,c_0_172])]),
[final] ).
cnf(i_0_348,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub]),
[final] ).
cnf(i_0_349,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub]),
[final] ).
cnf(i_0_350,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub]),
[final] ).
cnf(i_0_351,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub]),
[final] ).
cnf(i_0_352,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub]),
[final] ).
cnf(i_0_353,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub]),
[final] ).
cnf(i_0_354,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_datatype_sub]),
[final] ).
cnf(i_0_355,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range]),
[final] ).
cnf(i_0_356,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_range]),
[final] ).
cnf(i_0_357,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_range]),
[final] ).
cnf(i_0_358,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range]),
[final] ).
cnf(i_0_359,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range]),
[final] ).
cnf(i_0_360,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range]),
[final] ).
cnf(i_0_361,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range]),
[final] ).
cnf(i_0_362,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range]),
[final] ).
cnf(i_0_363,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_range]),
[final] ).
cnf(i_0_364,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003]),
[final] ).
cnf(i_0_365,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002]),
[final] ).
cnf(i_0_366,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001]),
[final] ).
cnf(i_0_367,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range]),
[final] ).
cnf(i_0_368,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_range]),
[final] ).
cnf(i_0_369,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_range_range]),
[final] ).
cnf(i_0_370,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_domain_range]),
[final] ).
cnf(i_0_371,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_type_range]),
[final] ).
cnf(i_0_372,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range]),
[final] ).
cnf(i_0_373,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_range]),
[final] ).
cnf(i_0_374,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain]),
[final] ).
cnf(i_0_375,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_domain]),
[final] ).
cnf(i_0_376,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain]),
[final] ).
cnf(i_0_377,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain]),
[final] ).
cnf(i_0_378,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain]),
[final] ).
cnf(i_0_379,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain]),
[final] ).
cnf(i_0_380,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain]),
[final] ).
cnf(i_0_381,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_domain]),
[final] ).
cnf(i_0_382,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain]),
[final] ).
cnf(i_0_383,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003]),
[final] ).
cnf(i_0_384,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002]),
[final] ).
cnf(i_0_385,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001]),
[final] ).
cnf(i_0_386,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain]),
[final] ).
cnf(i_0_387,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain]),
[final] ).
cnf(i_0_388,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_range_domain]),
[final] ).
cnf(i_0_389,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_domain_domain]),
[final] ).
cnf(i_0_390,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_type_domain]),
[final] ).
cnf(i_0_391,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain]),
[final] ).
cnf(i_0_392,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain]),
[final] ).
cnf(i_0_393,plain,
iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_394,plain,
iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_395,plain,
iext(uri_rdf_type,uri_ex_harry,esk19_0),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_396,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type]),
[final] ).
cnf(i_0_397,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_subject_type]),
[final] ).
cnf(i_0_398,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type]),
[final] ).
cnf(i_0_399,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_object_type]),
[final] ).
cnf(i_0_400,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003]),
[final] ).
cnf(i_0_401,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_003]),
[final] ).
cnf(i_0_402,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002]),
[final] ).
cnf(i_0_403,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_002]),
[final] ).
cnf(i_0_404,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001]),
[final] ).
cnf(i_0_405,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_001]),
[final] ).
cnf(i_0_406,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_property_type]),
[final] ).
cnf(i_0_407,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_value_type]),
[final] ).
cnf(i_0_408,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_type_type]),
[final] ).
cnf(i_0_409,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_rest_type]),
[final] ).
cnf(i_0_410,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_first_type]),
[final] ).
cnf(i_0_411,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdf_collection_nil_type]),
[final] ).
cnf(i_0_412,plain,
iext(uri_owl_unionOf,esk19_0,esk20_0),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_413,plain,
iext(uri_rdf_rest,esk21_0,uri_rdf_nil),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_414,plain,
iext(uri_rdf_rest,esk20_0,esk21_0),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_415,plain,
iext(uri_rdf_first,esk21_0,uri_ex_Falcon),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_416,plain,
iext(uri_rdf_first,esk20_0,uri_ex_Eagle),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_417,plain,
( lv(X2)
| ~ idc(X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_418,plain,
( lv(X1)
| ~ icext(uri_rdfs_Literal,X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_419,plain,
( ic(X1)
| ~ icext(uri_rdfs_Class,X1) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_420,plain,
~ icext(uri_owl_Nothing,X1),
inference(split_conjunct,[status(thm)],[i_0_195]),
[final] ).
cnf(i_0_421,plain,
( icext(uri_rdfs_Literal,X1)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_422,plain,
( icext(uri_rdfs_Class,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_423,plain,
icext(uri_rdfs_Resource,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_196,c_0_172])]),
[final] ).
cnf(i_0_424,plain,
icext(uri_owl_Thing,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_197,c_0_172])]),
[final] ).
cnf(i_0_425,plain,
( ip(X1)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_198]),
[final] ).
cnf(i_0_426,plain,
( ip(X1)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_199]),
[final] ).
cnf(i_0_427,plain,
( ip(X1)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_200]),
[final] ).
cnf(i_0_428,plain,
( ic(X1)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_201]),
[final] ).
cnf(i_0_429,plain,
ip(uri_owl_someValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_somevaluesfrom_type]),
[final] ).
cnf(i_0_430,plain,
ip(uri_owl_onProperty),
inference(split_conjunct,[status(thm)],[owl_prop_onproperty_type]),
[final] ).
cnf(i_0_431,plain,
ip(uri_owl_hasValue),
inference(split_conjunct,[status(thm)],[owl_prop_hasvalue_type]),
[final] ).
cnf(i_0_432,plain,
ip(uri_owl_allValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_allvaluesfrom_type]),
[final] ).
cnf(i_0_433,plain,
ip(uri_owl_unionOf),
inference(split_conjunct,[status(thm)],[owl_prop_unionof_type]),
[final] ).
cnf(i_0_434,plain,
ip(uri_owl_intersectionOf),
inference(split_conjunct,[status(thm)],[owl_prop_intersectionof_type]),
[final] ).
cnf(i_0_435,plain,
ip(uri_owl_complementOf),
inference(split_conjunct,[status(thm)],[owl_prop_complementof_type]),
[final] ).
cnf(i_0_436,plain,
ic(uri_owl_Thing),
inference(split_conjunct,[status(thm)],[owl_class_thing_type]),
[final] ).
cnf(i_0_437,plain,
ic(uri_owl_Nothing),
inference(split_conjunct,[status(thm)],[owl_class_nothing_type]),
[final] ).
cnf(i_0_438,plain,
~ iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon),
inference(scs_inference,[],[i_0_393,i_0_276]) ).
cnf(i_0_439,plain,
( ~ iext(uri_rdf_type,X1,uri_ex_Species)
| ~ iext(uri_rdf_type,uri_ex_harry,X1) ),
inference(rename_variables,[],[i_0_276]) ).
cnf(i_0_440,plain,
~ icext(uri_ex_Falcon,uri_ex_harry),
inference(scs_inference,[],[i_0_393,i_0_276,i_0_332]) ).
cnf(i_0_441,plain,
( iext(uri_rdf_type,X1,X2)
| ~ icext(X2,X1) ),
inference(rename_variables,[],[i_0_332]) ).
cnf(i_0_442,plain,
icext(uri_rdf_Property,uri_rdf_type),
inference(scs_inference,[],[i_0_408,i_0_393,i_0_276,i_0_332,i_0_286]) ).
cnf(i_0_443,plain,
( ~ iext(uri_rdf_type,X1,X2)
| icext(X2,X1) ),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_444,plain,
ip(uri_rdfs_isDefinedBy),
inference(scs_inference,[],[i_0_408,i_0_348,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300]) ).
cnf(i_0_445,plain,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_300]) ).
cnf(i_0_446,plain,
ip(uri_rdfs_seeAlso),
inference(scs_inference,[],[i_0_408,i_0_348,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302]) ).
cnf(i_0_447,plain,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_302]) ).
cnf(i_0_448,plain,
ip(uri_rdf_predicate),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303]) ).
cnf(i_0_449,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_450,plain,
ip(uri_rdfs_Resource),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304]) ).
cnf(i_0_451,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_452,plain,
ip(uri_rdfs_member),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_375,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305]) ).
cnf(i_0_453,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_454,plain,
ic(uri_rdf_XMLLiteral),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_375,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308]) ).
cnf(i_0_455,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_456,plain,
ic(uri_rdfs_Literal),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_375,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310]) ).
cnf(i_0_457,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X2) ),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_458,plain,
ic(uri_rdfs_Statement),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_393,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311]) ).
cnf(i_0_459,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ic(X2) ),
inference(rename_variables,[],[i_0_311]) ).
cnf(i_0_460,plain,
ic(esk19_0),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_393,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314]) ).
cnf(i_0_461,plain,
( ~ iext(uri_owl_unionOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_314]) ).
cnf(i_0_462,plain,
ip(uri_rdf_type),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_393,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324]) ).
cnf(i_0_463,plain,
( ~ iext(uri_rdf_type,X1,uri_rdf_Property)
| ip(X1) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_464,plain,
idc(uri_rdf_XMLLiteral),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_393,i_0_396,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327]) ).
cnf(i_0_465,plain,
( ~ iext(uri_rdf_type,X1,uri_rdfs_Datatype)
| idc(X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_466,plain,
ic(uri_rdf_Property),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_393,i_0_396,i_0_406,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328]) ).
cnf(i_0_467,plain,
( ~ iext(uri_rdf_type,X1,uri_rdfs_Class)
| ic(X1) ),
inference(rename_variables,[],[i_0_328]) ).
cnf(i_0_468,plain,
icext(uri_rdf_Property,uri_rdfs_isDefinedBy),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271]) ).
cnf(i_0_469,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_470,plain,
icext(uri_rdf_Property,uri_rdfs_seeAlso),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272]) ).
cnf(i_0_471,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X4,X3) ),
inference(rename_variables,[],[i_0_272]) ).
cnf(i_0_472,plain,
iext(uri_rdfs_subClassOf,uri_owl_Thing,uri_owl_Thing),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_424,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_436,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277]) ).
cnf(i_0_473,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_474,plain,
( ~ icext(X1,esk14_2(X2,X1))
| iext(uri_rdfs_subClassOf,X2,X1)
| ~ ic(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_475,plain,
iext(uri_rdfs_range,uri_owl_someValuesFrom,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_423,i_0_424,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_429,i_0_436,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278]) ).
cnf(i_0_476,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_477,plain,
( ~ icext(X1,esk13_2(X2,X1))
| iext(uri_rdfs_range,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_278]) ).
cnf(i_0_478,plain,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Thing),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_423,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_429,i_0_436,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279]) ).
cnf(i_0_479,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_480,plain,
( ~ icext(X1,esk10_2(X2,X1))
| iext(uri_rdfs_domain,X2,X1)
| ~ ip(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_481,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284]) ).
cnf(i_0_482,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_483,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(rename_variables,[],[i_0_284]) ).
cnf(i_0_484,plain,
~ iext(uri_owl_unionOf,uri_rdfs_Resource,esk21_0),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_476,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_415,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255]) ).
cnf(i_0_485,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_486,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_unionOf,X3,X1)
| icext(X2,X4)
| ~ icext(X3,X4) ),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_487,plain,
~ iext(uri_owl_intersectionOf,uri_rdfs_Resource,esk21_0),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_476,i_0_485,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_415,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255,i_0_256]) ).
cnf(i_0_488,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_489,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_intersectionOf,X3,X1)
| icext(X2,X4)
| ~ icext(X3,X4) ),
inference(rename_variables,[],[i_0_256]) ).
cnf(i_0_490,plain,
ic(uri_ex_Falcon),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_476,i_0_485,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255,i_0_256,i_0_248]) ).
cnf(i_0_491,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X1)
| ic(X2) ),
inference(rename_variables,[],[i_0_248]) ).
cnf(i_0_492,plain,
( iext(uri_rdfs_seeAlso,X1,X2)
| ~ iext(uri_rdfs_isDefinedBy,X1,X2) ),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_476,i_0_485,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255,i_0_256,i_0_248,i_0_266]) ).
cnf(i_0_493,plain,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(X2,X3,X4)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_266]) ).
cnf(i_0_494,plain,
( ~ iext(uri_rdfs_isDefinedBy,esk15_2(uri_owl_someValuesFrom,uri_rdfs_seeAlso),esk16_2(uri_owl_someValuesFrom,uri_rdfs_seeAlso))
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,uri_rdfs_seeAlso) ),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_423,i_0_476,i_0_485,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255,i_0_256,i_0_248,i_0_266,i_0_264]) ).
cnf(i_0_495,plain,
( ~ iext(X1,esk15_2(X2,X1),esk16_2(X2,X1))
| iext(uri_rdfs_subPropertyOf,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_264]) ).
cnf(i_0_496,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_497,plain,
( ~ iext(uri_rdfs_isDefinedBy,esk15_2(uri_owl_someValuesFrom,uri_rdfs_seeAlso),esk16_2(uri_owl_someValuesFrom,uri_rdfs_seeAlso))
| ~ iext(uri_owl_allValuesFrom,uri_owl_Nothing,uri_rdfs_Resource)
| ~ iext(uri_owl_onProperty,uri_owl_Nothing,X1) ),
inference(scs_inference,[],[i_0_356,i_0_408,i_0_420,i_0_482,i_0_423,i_0_476,i_0_485,i_0_488,i_0_424,i_0_473,i_0_348,i_0_349,i_0_367,i_0_374,i_0_375,i_0_386,i_0_393,i_0_396,i_0_406,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_429,i_0_436,i_0_437,i_0_276,i_0_332,i_0_286,i_0_300,i_0_302,i_0_303,i_0_304,i_0_305,i_0_308,i_0_310,i_0_311,i_0_314,i_0_324,i_0_327,i_0_328,i_0_271,i_0_272,i_0_277,i_0_278,i_0_279,i_0_284,i_0_255,i_0_256,i_0_248,i_0_266,i_0_264,i_0_216]) ).
cnf(i_0_498,plain,
~ iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle),
inference(scs_inference,[],[i_0_394,i_0_276]) ).
cnf(i_0_499,plain,
( ~ iext(uri_rdf_type,X1,uri_ex_Species)
| ~ iext(uri_rdf_type,uri_ex_harry,X1) ),
inference(rename_variables,[],[i_0_276]) ).
cnf(i_0_500,plain,
~ icext(uri_ex_Eagle,uri_ex_harry),
inference(scs_inference,[],[i_0_394,i_0_276,i_0_332]) ).
cnf(i_0_501,plain,
( iext(uri_rdf_type,X1,X2)
| ~ icext(X2,X1) ),
inference(rename_variables,[],[i_0_332]) ).
cnf(i_0_502,plain,
ip(uri_rdfs_label),
inference(scs_inference,[],[i_0_358,i_0_394,i_0_276,i_0_332,i_0_303]) ).
cnf(i_0_503,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_504,plain,
ip(uri_rdfs_Literal),
inference(scs_inference,[],[i_0_358,i_0_394,i_0_276,i_0_332,i_0_303,i_0_304]) ).
cnf(i_0_505,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_506,plain,
ic(uri_rdfs_Seq),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_394,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308]) ).
cnf(i_0_507,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_508,plain,
ic(uri_rdfs_Container),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_394,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310]) ).
cnf(i_0_509,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X2) ),
inference(rename_variables,[],[i_0_310]) ).
cnf(i_0_510,plain,
ic(uri_rdfs_Resource),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_376,i_0_394,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311]) ).
cnf(i_0_511,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ic(X2) ),
inference(rename_variables,[],[i_0_311]) ).
cnf(i_0_512,plain,
ip(uri_rdf_subject),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_376,i_0_394,i_0_397,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324]) ).
cnf(i_0_513,plain,
( ~ iext(uri_rdf_type,X1,uri_rdf_Property)
| ip(X1) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_514,plain,
icext(uri_ex_Species,uri_ex_Eagle),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_376,i_0_394,i_0_397,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286]) ).
cnf(i_0_515,plain,
( ~ iext(uri_rdf_type,X1,X2)
| icext(X2,X1) ),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_516,plain,
ip(uri_rdfs_comment),
inference(scs_inference,[],[i_0_350,i_0_358,i_0_376,i_0_379,i_0_394,i_0_397,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305]) ).
cnf(i_0_517,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_518,plain,
icext(uri_rdfs_Class,uri_owl_Thing),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271]) ).
cnf(i_0_519,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_520,plain,
icext(uri_rdfs_Class,uri_rdfs_Class),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272]) ).
cnf(i_0_521,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X4,X3) ),
inference(rename_variables,[],[i_0_272]) ).
cnf(i_0_522,plain,
iext(uri_rdfs_range,uri_owl_onProperty,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_423,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278]) ).
cnf(i_0_523,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_524,plain,
( ~ icext(X1,esk13_2(X2,X1))
| iext(uri_rdfs_range,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_278]) ).
cnf(i_0_525,plain,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_423,i_0_523,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279]) ).
cnf(i_0_526,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_527,plain,
( ~ icext(X1,esk10_2(X2,X1))
| iext(uri_rdfs_domain,X2,X1)
| ~ ip(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_528,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdf_XMLLiteral),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_420,i_0_423,i_0_523,i_0_437,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284]) ).
cnf(i_0_529,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_530,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(rename_variables,[],[i_0_284]) ).
cnf(i_0_531,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_420,i_0_423,i_0_523,i_0_526,i_0_437,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277]) ).
cnf(i_0_532,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_533,plain,
( ~ icext(X1,esk14_2(X2,X1))
| iext(uri_rdfs_subClassOf,X2,X1)
| ~ ic(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_534,plain,
ic(uri_ex_Eagle),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_420,i_0_423,i_0_523,i_0_526,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247]) ).
cnf(i_0_535,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_owl_unionOf,X4,X2)
| ~ iext(uri_rdf_rest,X2,X1)
| ~ iext(uri_rdf_first,X1,X5)
| ic(X3) ),
inference(rename_variables,[],[i_0_247]) ).
cnf(i_0_536,plain,
~ iext(uri_rdf_first,esk21_0,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228]) ).
cnf(i_0_537,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_538,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_539,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ icext(X2,esk6_3(X2,X1,X3))
| ~ icext(X3,esk6_3(X2,X1,X3))
| ~ iext(uri_rdf_first,X1,X3)
| iext(uri_owl_unionOf,X2,X1)
| ~ ic(X2)
| ~ ic(X3) ),
inference(rename_variables,[],[i_0_228]) ).
cnf(i_0_540,plain,
~ iext(uri_owl_intersectionOf,uri_rdfs_Resource,esk20_0),
inference(scs_inference,[],[i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242]) ).
cnf(i_0_541,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_542,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_owl_intersectionOf,X4,X2)
| ~ iext(uri_rdf_rest,X2,X1)
| ~ iext(uri_rdf_first,X1,X5)
| icext(X3,X6)
| ~ icext(X4,X6) ),
inference(rename_variables,[],[i_0_242]) ).
cnf(i_0_543,plain,
~ icext(esk19_0,uri_ex_harry),
inference(scs_inference,[],[i_0_440,i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242,i_0_241]) ).
cnf(i_0_544,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_first,X1,X4)
| ~ iext(uri_owl_unionOf,X5,X2)
| ~ iext(uri_rdf_rest,X2,X1)
| icext(X3,X6)
| icext(X4,X6)
| ~ icext(X5,X6) ),
inference(rename_variables,[],[i_0_241]) ).
cnf(i_0_545,plain,
ic(uri_rdfs_Class),
inference(scs_inference,[],[i_0_440,i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242,i_0_241,i_0_419]) ).
cnf(i_0_546,plain,
( ~ icext(uri_rdfs_Class,X1)
| ic(X1) ),
inference(rename_variables,[],[i_0_419]) ).
cnf(i_0_547,plain,
( iext(uri_rdfs_subPropertyOf,X1,uri_rdfs_seeAlso)
| ~ iext(uri_rdfs_subPropertyOf,X1,uri_rdfs_isDefinedBy) ),
inference(scs_inference,[],[i_0_440,i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_348,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242,i_0_241,i_0_419,i_0_267]) ).
cnf(i_0_548,plain,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(uri_rdfs_subPropertyOf,X3,X2)
| ~ iext(uri_rdfs_subPropertyOf,X3,X1) ),
inference(rename_variables,[],[i_0_267]) ).
cnf(i_0_549,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Literal),
inference(scs_inference,[],[i_0_440,i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_349,i_0_348,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242,i_0_241,i_0_419,i_0_267,i_0_268]) ).
cnf(i_0_550,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| iext(uri_rdfs_subClassOf,X3,X2)
| ~ iext(uri_rdfs_subClassOf,X3,X1) ),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_551,plain,
( iext(uri_rdfs_seeAlso,X1,uri_rdfs_Resource)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdfs_isDefinedBy) ),
inference(scs_inference,[],[i_0_347,i_0_440,i_0_472,i_0_350,i_0_358,i_0_369,i_0_376,i_0_379,i_0_387,i_0_394,i_0_397,i_0_430,i_0_450,i_0_454,i_0_484,i_0_420,i_0_423,i_0_523,i_0_526,i_0_532,i_0_538,i_0_414,i_0_416,i_0_437,i_0_412,i_0_413,i_0_415,i_0_349,i_0_348,i_0_276,i_0_332,i_0_303,i_0_304,i_0_308,i_0_310,i_0_311,i_0_324,i_0_286,i_0_305,i_0_271,i_0_272,i_0_278,i_0_279,i_0_284,i_0_277,i_0_247,i_0_228,i_0_242,i_0_241,i_0_419,i_0_267,i_0_268,i_0_266]) ).
cnf(i_0_552,plain,
( ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(X2,X3,X4)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_266]) ).
cnf(i_0_553,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_555,plain,
ic(uri_rdf_List),
inference(scs_inference,[],[i_0_391,i_0_311]) ).
cnf(i_0_556,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ic(X2) ),
inference(rename_variables,[],[i_0_311]) ).
cnf(i_0_557,plain,
ip(uri_rdf_value),
inference(scs_inference,[],[i_0_391,i_0_398,i_0_311,i_0_324]) ).
cnf(i_0_558,plain,
( ~ iext(uri_rdf_type,X1,uri_rdf_Property)
| ip(X1) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_559,plain,
ip(uri_rdf__3),
inference(scs_inference,[],[i_0_364,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303]) ).
cnf(i_0_560,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_561,plain,
ip(uri_rdfs_Class),
inference(scs_inference,[],[i_0_364,i_0_368,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303,i_0_304]) ).
cnf(i_0_562,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_563,plain,
ic(uri_rdfs_ContainerMembershipProperty),
inference(scs_inference,[],[i_0_351,i_0_364,i_0_368,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308]) ).
cnf(i_0_564,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_565,plain,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_364,i_0_368,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286]) ).
cnf(i_0_566,plain,
( ~ iext(uri_rdf_type,X1,X2)
| icext(X2,X1) ),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_567,plain,
ip(uri_rdf_object),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_364,i_0_368,i_0_382,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305]) ).
cnf(i_0_568,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_569,plain,
icext(uri_rdf_Property,uri_rdfs_member),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_357,i_0_364,i_0_368,i_0_382,i_0_388,i_0_391,i_0_398,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271]) ).
cnf(i_0_570,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_571,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_357,i_0_364,i_0_368,i_0_382,i_0_388,i_0_391,i_0_398,i_0_528,i_0_531,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268]) ).
cnf(i_0_572,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| iext(uri_rdfs_subClassOf,X3,X2)
| ~ iext(uri_rdfs_subClassOf,X3,X1) ),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_573,plain,
icext(uri_rdfs_Class,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_528,i_0_531,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272]) ).
cnf(i_0_574,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X4,X3) ),
inference(rename_variables,[],[i_0_272]) ).
cnf(i_0_575,plain,
icext(uri_rdfs_Class,uri_rdf_XMLLiteral),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_528,i_0_531,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282]) ).
cnf(i_0_576,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| icext(X2,X3)
| ~ icext(X1,X3) ),
inference(rename_variables,[],[i_0_282]) ).
cnf(i_0_577,plain,
iext(uri_rdfs_range,uri_owl_hasValue,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_528,i_0_531,i_0_450,i_0_423,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278]) ).
cnf(i_0_578,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_579,plain,
( ~ icext(X1,esk13_2(X2,X1))
| iext(uri_rdfs_range,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_278]) ).
cnf(i_0_580,plain,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Thing),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_528,i_0_531,i_0_424,i_0_450,i_0_423,i_0_436,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279]) ).
cnf(i_0_581,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_582,plain,
( ~ icext(X1,esk10_2(X2,X1))
| iext(uri_rdfs_domain,X2,X1)
| ~ ip(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_583,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_owl_Thing),
inference(scs_inference,[],[i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_450,i_0_423,i_0_436,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277]) ).
cnf(i_0_584,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_585,plain,
( ~ icext(X1,esk14_2(X2,X1))
| iext(uri_rdfs_subClassOf,X2,X1)
| ~ ic(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_586,plain,
~ iext(uri_owl_unionOf,uri_owl_Thing,esk21_0),
inference(scs_inference,[],[i_0_440,i_0_413,i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_450,i_0_423,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255]) ).
cnf(i_0_587,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_588,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_unionOf,X3,X1)
| icext(X2,X4)
| ~ icext(X3,X4) ),
inference(rename_variables,[],[i_0_255]) ).
cnf(i_0_589,plain,
~ iext(uri_owl_intersectionOf,uri_owl_Thing,esk21_0),
inference(scs_inference,[],[i_0_440,i_0_413,i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_450,i_0_423,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256]) ).
cnf(i_0_590,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_591,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_intersectionOf,X3,X1)
| icext(X2,X4)
| ~ icext(X3,X4) ),
inference(rename_variables,[],[i_0_256]) ).
cnf(i_0_592,plain,
~ iext(uri_rdf_first,esk21_0,uri_owl_Thing),
inference(scs_inference,[],[i_0_440,i_0_413,i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_450,i_0_423,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229]) ).
cnf(i_0_593,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_594,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_595,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ icext(X2,esk2_3(X2,X1,X3))
| ~ icext(X3,esk2_3(X2,X1,X3))
| ~ iext(uri_rdf_first,X1,X3)
| iext(uri_owl_intersectionOf,X2,X1)
| ~ ic(X2)
| ~ ic(X3) ),
inference(rename_variables,[],[i_0_229]) ).
cnf(i_0_596,plain,
~ iext(uri_owl_intersectionOf,uri_owl_Thing,esk20_0),
inference(scs_inference,[],[i_0_440,i_0_413,i_0_396,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_450,i_0_423,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243]) ).
cnf(i_0_597,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_598,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| ~ iext(uri_rdf_first,X1,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X1)
| icext(X2,X6)
| ~ icext(X3,X6) ),
inference(rename_variables,[],[i_0_243]) ).
cnf(i_0_599,plain,
( lv(uri_owl_Thing)
| ~ idc(uri_rdfs_Class) ),
inference(scs_inference,[],[i_0_440,i_0_413,i_0_396,i_0_518,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_450,i_0_423,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243,i_0_417]) ).
cnf(i_0_600,plain,
( ~ icext(X1,X2)
| lv(X2)
| ~ idc(X1) ),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_601,plain,
( ~ iext(uri_owl_allValuesFrom,uri_ex_Eagle,uri_owl_Thing)
| ~ iext(uri_owl_onProperty,uri_ex_Eagle,X1) ),
inference(scs_inference,[],[i_0_500,i_0_440,i_0_413,i_0_396,i_0_518,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_597,i_0_450,i_0_423,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243,i_0_417,i_0_216]) ).
cnf(i_0_602,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_603,plain,
( ~ icext(X1,esk17_4(X2,X3,X1,X4))
| ~ iext(uri_owl_allValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3)
| icext(X2,X4) ),
inference(rename_variables,[],[i_0_216]) ).
cnf(i_0_604,plain,
( ~ iext(uri_owl_someValuesFrom,uri_rdfs_Class,uri_owl_Nothing)
| ~ iext(uri_owl_onProperty,uri_rdfs_Class,X1) ),
inference(scs_inference,[],[i_0_500,i_0_440,i_0_413,i_0_396,i_0_518,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_597,i_0_450,i_0_420,i_0_423,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243,i_0_417,i_0_216,i_0_219]) ).
cnf(i_0_605,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_606,plain,
( icext(X1,esk18_4(X2,X3,X1,X4))
| ~ iext(uri_owl_someValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3)
| ~ icext(X2,X4) ),
inference(rename_variables,[],[i_0_219]) ).
cnf(i_0_607,plain,
( iext(uri_owl_unionOf,uri_owl_Nothing,esk21_0)
| ~ iext(uri_rdf_first,esk21_0,uri_owl_Nothing) ),
inference(scs_inference,[],[i_0_500,i_0_440,i_0_413,i_0_396,i_0_518,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_597,i_0_450,i_0_420,i_0_605,i_0_423,i_0_437,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243,i_0_417,i_0_216,i_0_219,i_0_239]) ).
cnf(i_0_608,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_609,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_610,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| icext(X2,esk6_3(X2,X1,X3))
| icext(X3,esk6_3(X2,X1,X3))
| iext(uri_owl_unionOf,X2,X1)
| ~ iext(uri_rdf_first,X1,X3)
| ~ ic(X2)
| ~ ic(X3) ),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_611,plain,
( iext(uri_owl_intersectionOf,uri_owl_Nothing,esk21_0)
| ~ iext(uri_rdf_first,esk21_0,uri_owl_Nothing) ),
inference(scs_inference,[],[i_0_500,i_0_440,i_0_413,i_0_396,i_0_518,i_0_351,i_0_354,i_0_357,i_0_364,i_0_368,i_0_370,i_0_377,i_0_382,i_0_388,i_0_391,i_0_398,i_0_431,i_0_456,i_0_528,i_0_531,i_0_424,i_0_581,i_0_584,i_0_587,i_0_590,i_0_594,i_0_597,i_0_450,i_0_420,i_0_605,i_0_609,i_0_423,i_0_437,i_0_414,i_0_416,i_0_436,i_0_415,i_0_311,i_0_324,i_0_303,i_0_304,i_0_308,i_0_286,i_0_305,i_0_271,i_0_268,i_0_272,i_0_282,i_0_278,i_0_279,i_0_277,i_0_255,i_0_256,i_0_229,i_0_243,i_0_417,i_0_216,i_0_219,i_0_239,i_0_240]) ).
cnf(i_0_612,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_613,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_614,plain,
( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
| icext(X2,esk2_3(X2,X1,X3))
| icext(X3,esk2_3(X2,X1,X3))
| iext(uri_owl_intersectionOf,X2,X1)
| ~ iext(uri_rdf_first,X1,X3)
| ~ ic(X2)
| ~ ic(X3) ),
inference(rename_variables,[],[i_0_240]) ).
cnf(i_0_616,plain,
ip(uri_rdf__2),
inference(scs_inference,[],[i_0_403,i_0_324]) ).
cnf(i_0_617,plain,
( ~ iext(uri_rdf_type,X1,uri_rdf_Property)
| ip(X1) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_618,plain,
ic(uri_rdf_Bag),
inference(scs_inference,[],[i_0_352,i_0_403,i_0_324,i_0_308]) ).
cnf(i_0_619,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_620,plain,
icext(uri_rdfs_Class,uri_rdf_Property),
inference(scs_inference,[],[i_0_406,i_0_352,i_0_403,i_0_324,i_0_308,i_0_286]) ).
cnf(i_0_621,plain,
( ~ iext(uri_rdf_type,X1,X2)
| icext(X2,X1) ),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_622,plain,
ip(uri_rdf__1),
inference(scs_inference,[],[i_0_406,i_0_352,i_0_366,i_0_403,i_0_324,i_0_308,i_0_286,i_0_303]) ).
cnf(i_0_623,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_624,plain,
ip(uri_rdfs_domain),
inference(scs_inference,[],[i_0_406,i_0_352,i_0_366,i_0_389,i_0_403,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305]) ).
cnf(i_0_625,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_626,plain,
ip(uri_rdf_List),
inference(scs_inference,[],[i_0_406,i_0_352,i_0_366,i_0_372,i_0_389,i_0_403,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304]) ).
cnf(i_0_627,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_628,plain,
icext(uri_rdf_Property,uri_rdfs_domain),
inference(scs_inference,[],[i_0_406,i_0_352,i_0_366,i_0_372,i_0_389,i_0_403,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271]) ).
cnf(i_0_629,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_630,plain,
icext(uri_rdf_List,uri_rdf_nil),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_366,i_0_372,i_0_389,i_0_403,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272]) ).
cnf(i_0_631,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X4,X3) ),
inference(rename_variables,[],[i_0_272]) ).
cnf(i_0_632,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Statement),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_458,i_0_437,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284]) ).
cnf(i_0_633,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_634,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(rename_variables,[],[i_0_284]) ).
cnf(i_0_635,plain,
iext(uri_rdfs_range,uri_owl_allValuesFrom,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_450,i_0_423,i_0_437,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278]) ).
cnf(i_0_636,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_637,plain,
( ~ icext(X1,esk13_2(X2,X1))
| iext(uri_rdfs_range,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_278]) ).
cnf(i_0_638,plain,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Thing),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_450,i_0_423,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279]) ).
cnf(i_0_639,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_640,plain,
( ~ icext(X1,esk10_2(X2,X1))
| iext(uri_rdfs_domain,X2,X1)
| ~ ip(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_641,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_owl_Thing),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_639,i_0_450,i_0_423,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279,i_0_277]) ).
cnf(i_0_642,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_643,plain,
( ~ icext(X1,esk14_2(X2,X1))
| iext(uri_rdfs_subClassOf,X2,X1)
| ~ ic(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_644,plain,
( lv(uri_rdfs_Class)
| ~ idc(uri_rdfs_Class) ),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_352,i_0_520,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_639,i_0_450,i_0_423,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417]) ).
cnf(i_0_645,plain,
( ~ icext(X1,X2)
| lv(X2)
| ~ idc(X1) ),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_646,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Literal)
| ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing) ),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_549,i_0_352,i_0_520,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_639,i_0_450,i_0_423,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_268]) ).
cnf(i_0_647,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| iext(uri_rdfs_subClassOf,X3,X2)
| ~ iext(uri_rdfs_subClassOf,X3,X1) ),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_648,plain,
( icext(uri_rdfs_Container,X1)
| ~ icext(uri_rdf_Bag,X1) ),
inference(scs_inference,[],[i_0_413,i_0_406,i_0_549,i_0_352,i_0_520,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_639,i_0_450,i_0_423,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_268,i_0_282]) ).
cnf(i_0_649,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| icext(X2,X3)
| ~ icext(X1,X3) ),
inference(rename_variables,[],[i_0_282]) ).
cnf(i_0_650,plain,
( ~ iext(uri_owl_allValuesFrom,uri_ex_Eagle,uri_rdfs_Resource)
| ~ iext(uri_owl_onProperty,uri_ex_Eagle,X1) ),
inference(scs_inference,[],[i_0_500,i_0_413,i_0_406,i_0_549,i_0_352,i_0_520,i_0_420,i_0_366,i_0_372,i_0_389,i_0_403,i_0_432,i_0_458,i_0_424,i_0_639,i_0_450,i_0_423,i_0_636,i_0_437,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_272,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_268,i_0_282,i_0_216]) ).
cnf(i_0_651,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_652,plain,
( ~ icext(X1,esk17_4(X2,X3,X1,X4))
| ~ iext(uri_owl_allValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3)
| icext(X2,X4) ),
inference(rename_variables,[],[i_0_216]) ).
cnf(i_0_654,plain,
ip(uri_rdf_rest),
inference(scs_inference,[],[i_0_409,i_0_324]) ).
cnf(i_0_655,plain,
( ~ iext(uri_rdf_type,X1,uri_rdf_Property)
| ip(X1) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_656,plain,
ic(uri_rdfs_Datatype),
inference(scs_inference,[],[i_0_354,i_0_409,i_0_324,i_0_308]) ).
cnf(i_0_657,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_658,plain,
icext(uri_ex_Species,uri_ex_Falcon),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_409,i_0_324,i_0_308,i_0_286]) ).
cnf(i_0_659,plain,
( ~ iext(uri_rdf_type,X1,X2)
| icext(X2,X1) ),
inference(rename_variables,[],[i_0_286]) ).
cnf(i_0_660,plain,
ip(uri_rdf_first),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_373,i_0_409,i_0_324,i_0_308,i_0_286,i_0_303]) ).
cnf(i_0_661,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_662,plain,
ip(uri_rdfs_subPropertyOf),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_386,i_0_373,i_0_409,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305]) ).
cnf(i_0_663,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| ip(X1) ),
inference(rename_variables,[],[i_0_305]) ).
cnf(i_0_664,plain,
ip(uri_rdf_Property),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_386,i_0_373,i_0_409,i_0_367,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304]) ).
cnf(i_0_665,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| ip(X2) ),
inference(rename_variables,[],[i_0_304]) ).
cnf(i_0_666,plain,
icext(uri_rdf_List,esk20_0),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_392,i_0_386,i_0_373,i_0_409,i_0_367,i_0_416,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271]) ).
cnf(i_0_667,plain,
( ~ iext(uri_rdfs_domain,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X3,X4) ),
inference(rename_variables,[],[i_0_271]) ).
cnf(i_0_668,plain,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,esk19_0),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_392,i_0_386,i_0_420,i_0_373,i_0_409,i_0_460,i_0_367,i_0_437,i_0_416,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284]) ).
cnf(i_0_669,plain,
~ icext(uri_owl_Nothing,X1),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_670,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(rename_variables,[],[i_0_284]) ).
cnf(i_0_671,plain,
iext(uri_rdfs_range,uri_owl_unionOf,uri_rdfs_Resource),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_392,i_0_386,i_0_420,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_450,i_0_423,i_0_437,i_0_416,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278]) ).
cnf(i_0_672,plain,
icext(uri_rdfs_Resource,X1),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_673,plain,
( ~ icext(X1,esk13_2(X2,X1))
| iext(uri_rdfs_range,X2,X1)
| ~ ip(X2)
| ~ ip(X1) ),
inference(rename_variables,[],[i_0_278]) ).
cnf(i_0_674,plain,
iext(uri_rdfs_domain,uri_owl_unionOf,uri_owl_Thing),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_392,i_0_386,i_0_420,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279]) ).
cnf(i_0_675,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_676,plain,
( ~ icext(X1,esk10_2(X2,X1))
| iext(uri_rdfs_domain,X2,X1)
| ~ ip(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_279]) ).
cnf(i_0_677,plain,
iext(uri_rdfs_subClassOf,esk19_0,uri_owl_Thing),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_392,i_0_386,i_0_420,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_675,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279,i_0_277]) ).
cnf(i_0_678,plain,
icext(uri_owl_Thing,X1),
inference(rename_variables,[],[i_0_424]) ).
cnf(i_0_679,plain,
( ~ icext(X1,esk14_2(X2,X1))
| iext(uri_rdfs_subClassOf,X2,X1)
| ~ ic(X2)
| ~ ic(X1) ),
inference(rename_variables,[],[i_0_277]) ).
cnf(i_0_680,plain,
( lv(uri_rdf_XMLLiteral)
| ~ idc(uri_rdfs_Class) ),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_575,i_0_392,i_0_386,i_0_420,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_675,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417]) ).
cnf(i_0_681,plain,
( ~ icext(X1,X2)
| lv(X2)
| ~ idc(X1) ),
inference(rename_variables,[],[i_0_417]) ).
cnf(i_0_682,plain,
( icext(uri_rdfs_Literal,X1)
| ~ iext(uri_rdfs_comment,X2,X1) ),
inference(scs_inference,[],[i_0_354,i_0_393,i_0_575,i_0_392,i_0_386,i_0_420,i_0_361,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_675,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_272]) ).
cnf(i_0_683,plain,
( ~ iext(uri_rdfs_range,X1,X2)
| icext(X2,X3)
| ~ iext(X1,X4,X3) ),
inference(rename_variables,[],[i_0_272]) ).
cnf(i_0_684,plain,
( icext(uri_rdfs_Literal,X1)
| ~ icext(uri_rdf_XMLLiteral,X1) ),
inference(scs_inference,[],[i_0_354,i_0_349,i_0_393,i_0_575,i_0_392,i_0_386,i_0_420,i_0_361,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_675,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_272,i_0_282]) ).
cnf(i_0_685,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| icext(X2,X3)
| ~ icext(X1,X3) ),
inference(rename_variables,[],[i_0_282]) ).
cnf(i_0_686,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,X1,uri_rdfs_Datatype) ),
inference(scs_inference,[],[i_0_354,i_0_349,i_0_393,i_0_575,i_0_392,i_0_386,i_0_420,i_0_361,i_0_373,i_0_409,i_0_433,i_0_460,i_0_367,i_0_424,i_0_675,i_0_450,i_0_423,i_0_437,i_0_416,i_0_436,i_0_324,i_0_308,i_0_286,i_0_303,i_0_305,i_0_304,i_0_271,i_0_284,i_0_278,i_0_279,i_0_277,i_0_417,i_0_272,i_0_282,i_0_268]) ).
cnf(i_0_687,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| iext(uri_rdfs_subClassOf,X3,X2)
| ~ iext(uri_rdfs_subClassOf,X3,X1) ),
inference(rename_variables,[],[i_0_268]) ).
cnf(i_0_689,plain,
ic(uri_rdf_Alt),
inference(scs_inference,[],[i_0_353,i_0_308]) ).
cnf(i_0_690,plain,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ic(X1) ),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_691,plain,
$false,
inference(scs_inference,[],[i_0_353,i_0_543,i_0_395,i_0_308,i_0_286]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWB014+3 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n004.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 04:08:17 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 1.30/1.60 % Version : CSE_E---1.7
% 1.30/1.60 % Problem : theBenchmark.p
% 1.30/1.60 % SZS status Theorem for theBenchmark.p
% 1.30/1.60 % SZS output start CNFRefutation
% See solution above
% 1.99/2.35 % Total time : 1.271s
%------------------------------------------------------------------------------