Vampire-SAT---5.0.1.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : SWB025+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT

% Computer : n001.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 01:00:46 PM UTC 2026

% Result   : CounterSatisfiable 0.72s 0.63s
% Output   : Saturation 0.72s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u477,negated_conjecture,
    ~ iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice) ).

cnf(u682,axiom,
    lv(X0) ).

cnf(u690,axiom,
    ( lv(X0)
    | ~ ic(X0) ) ).

cnf(u735,axiom,
    lv(uri_rdf_nil) ).

cnf(u746,axiom,
    lv(uri_rdf_first) ).

cnf(u757,axiom,
    lv(uri_rdf_rest) ).

cnf(u764,axiom,
    lv(uri_rdf_type) ).

cnf(u773,axiom,
    lv(uri_rdf__1) ).

cnf(u786,axiom,
    lv(uri_rdf__2) ).

cnf(u795,axiom,
    lv(uri_rdf__3) ).

cnf(u804,axiom,
    lv(uri_rdf_object) ).

cnf(u811,axiom,
    lv(uri_rdf_value) ).

cnf(u818,axiom,
    lv(uri_rdf_subject) ).

cnf(u825,axiom,
    lv(uri_rdf_XMLLiteral) ).

cnf(u869,axiom,
    iext(uri_owl_unionOf,uri_owl_Ontology,uri_rdf_nil) ).

cnf(u879,axiom,
    ioxp(sK4(uri_owl_OntologyProperty)) ).

cnf(u892,axiom,
    iodp(sK4(uri_owl_DatatypeProperty)) ).

cnf(u909,axiom,
    iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).

cnf(u922,axiom,
    iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_member) ).

cnf(u925,axiom,
    ~ iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).

cnf(u931,axiom,
    lv(sK4(uri_rdfs_Literal)) ).

cnf(u934,axiom,
    ~ iext(uri_owl_unionOf,uri_rdfs_Literal,uri_rdf_nil) ).

cnf(u940,axiom,
    ip(sK4(uri_rdf_Property)) ).

cnf(u943,axiom,
    ~ iext(uri_owl_unionOf,uri_rdf_Property,uri_rdf_nil) ).

cnf(u949,axiom,
    idc(sK4(uri_rdfs_Datatype)) ).

cnf(u952,axiom,
    ~ iext(uri_owl_unionOf,uri_rdfs_Datatype,uri_rdf_nil) ).

cnf(u958,axiom,
    iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),uri_rdfs_Literal) ).

cnf(u963,axiom,
    ic(sK4(uri_rdfs_Class)) ).

cnf(u966,axiom,
    ~ iext(uri_owl_unionOf,uri_rdfs_Class,uri_rdf_nil) ).

cnf(u971,axiom,
    ( ~ ip(X0)
    | lv(X0) ) ).

cnf(u976,axiom,
    lv(uri_rdf_Property) ).

cnf(u1115,axiom,
    iext(uri_owl_unionOf,uri_rdf_Alt,uri_rdf_nil) ).

cnf(u1132,axiom,
    iext(uri_owl_unionOf,uri_rdf_Bag,uri_rdf_nil) ).

cnf(u1156,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Seq,uri_rdf_nil) ).

cnf(u1173,axiom,
    iext(uri_owl_unionOf,uri_rdf_XMLLiteral,uri_rdf_nil) ).

cnf(u1190,axiom,
    iext(uri_owl_unionOf,sK4(uri_rdfs_Datatype),uri_rdf_nil) ).

cnf(u1342,axiom,
    ~ ix(X0) ).

cnf(u1354,axiom,
    icext(uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u1596,axiom,
    iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).

cnf(u1605,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).

cnf(u1986,axiom,
    icext(sK14(uri_owl_complementOf,uri_rdf_type),sK14(uri_owl_complementOf,uri_rdf_type)) ).

cnf(u2130,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasFather,sK19) ).

cnf(u2143,axiom,
    icext(uri_ex_hasFather,sK1(sK4(uri_rdfs_Datatype),uri_ex_hasFather)) ).

cnf(u2147,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_XMLLiteral,sK19) ).

cnf(u2152,axiom,
    icext(uri_ex_hasFather,sK1(uri_rdf_XMLLiteral,uri_ex_hasFather)) ).

cnf(u2161,axiom,
    icext(uri_ex_hasFather,sK1(uri_rdfs_Seq,uri_ex_hasFather)) ).

cnf(u2166,axiom,
    iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),uri_rdfs_member) ).

cnf(u2178,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Bag,sK19) ).

cnf(u2183,axiom,
    icext(uri_ex_hasFather,sK1(uri_rdf_Bag,uri_ex_hasFather)) ).

cnf(u2187,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Alt,sK19) ).

cnf(u2192,axiom,
    icext(uri_ex_hasFather,sK1(uri_rdf_Alt,uri_ex_hasFather)) ).

cnf(u2196,axiom,
    ~ iext(uri_owl_intersectionOf,uri_owl_Ontology,sK19) ).

cnf(u2201,axiom,
    icext(uri_ex_hasFather,sK1(uri_owl_Ontology,uri_ex_hasFather)) ).

cnf(u2206,axiom,
    ioxp(sK1(uri_owl_OntologyProperty,uri_ex_hasFather)) ).

cnf(u2223,axiom,
    iext(uri_owl_intersectionOf,uri_owl_DatatypeProperty,sK19) ).

cnf(u2227,axiom,
    icext(uri_ex_hasFather,sK1(uri_owl_DatatypeProperty,uri_ex_hasFather)) ).

cnf(u2236,axiom,
    icext(uri_ex_hasFather,sK1(uri_owl_AnnotationProperty,uri_ex_hasFather)) ).

cnf(u2249,axiom,
    icext(uri_ex_hasFather,sK1(uri_rdfs_Datatype,uri_ex_hasFather)) ).

cnf(u2258,axiom,
    icext(uri_ex_hasFather,sK1(uri_owl_Nothing,uri_ex_hasFather)) ).

cnf(u2394,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_intersectionOf,X4,X1)
    | ~ icext(X4,X3)
    | icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2401,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_intersectionOf,X4,X1)
    | ~ icext(X4,X3)
    | icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2430,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_unionOf,X4,X1)
    | icext(X4,X3)
    | ~ icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2434,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_unionOf,X4,X1)
    | icext(X4,X3)
    | ~ icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2462,axiom,
    iext(uri_owl_intersectionOf,sK22,sK21) ).

cnf(u2475,axiom,
    icext(sK22,sK1(sK4(uri_rdfs_Datatype),sK22)) ).

cnf(u2479,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_XMLLiteral,sK21) ).

cnf(u2484,axiom,
    icext(sK22,sK1(uri_rdf_XMLLiteral,sK22)) ).

cnf(u2493,axiom,
    icext(sK22,sK1(uri_rdfs_Seq,sK22)) ).

cnf(u2498,axiom,
    iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,sK22),uri_rdfs_member) ).

cnf(u2510,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Bag,sK21) ).

cnf(u2515,axiom,
    icext(sK22,sK1(uri_rdf_Bag,sK22)) ).

cnf(u2519,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Alt,sK21) ).

cnf(u2524,axiom,
    icext(sK22,sK1(uri_rdf_Alt,sK22)) ).

cnf(u2528,axiom,
    ~ iext(uri_owl_intersectionOf,uri_owl_Ontology,sK21) ).

cnf(u2533,axiom,
    icext(sK22,sK1(uri_owl_Ontology,sK22)) ).

cnf(u2538,axiom,
    ioxp(sK1(uri_owl_OntologyProperty,sK22)) ).

cnf(u2555,axiom,
    iext(uri_owl_intersectionOf,uri_owl_DatatypeProperty,sK21) ).

cnf(u2559,axiom,
    icext(sK22,sK1(uri_owl_DatatypeProperty,sK22)) ).

cnf(u2568,axiom,
    icext(sK22,sK1(uri_owl_AnnotationProperty,sK22)) ).

cnf(u2581,axiom,
    icext(sK22,sK1(uri_rdfs_Datatype,sK22)) ).

cnf(u2590,axiom,
    icext(sK22,sK1(uri_owl_Nothing,sK22)) ).

cnf(u2733,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | ~ icext(X6,X5)
    | icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2737,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | ~ icext(X6,X5)
    | icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2744,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | ~ icext(X6,X5)
    | icext(X4,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2748,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | ~ icext(X6,X5)
    | icext(X4,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2756,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2760,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2766,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X4,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2770,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X4,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2799,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Literal,sK19) ).

cnf(u2808,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Resource,sK19) ).

cnf(u2817,axiom,
    iext(uri_owl_intersectionOf,uri_rdf_Property,sK19) ).

cnf(u2826,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Class,sK19) ).

cnf(u2835,axiom,
    iext(uri_owl_intersectionOf,uri_owl_Thing,sK19) ).

cnf(u2911,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X4,X5)
    | ~ icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u2938,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasFather,sK21) ).

cnf(u2947,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Literal,sK21) ).

cnf(u2956,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Resource,sK21) ).

cnf(u2965,axiom,
    iext(uri_owl_intersectionOf,uri_rdf_Property,sK21) ).

cnf(u2974,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Class,sK21) ).

cnf(u2983,axiom,
    iext(uri_owl_intersectionOf,uri_owl_Thing,sK21) ).

cnf(u3193,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | icext(X4,X3)
    | ~ iext(uri_owl_unionOf,X4,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3201,axiom,
    ( ~ iext(uri_owl_unionOf,X0,sK18)
    | icext(X0,X1) ) ).

cnf(u3208,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | icext(X4,X3)
    | ~ iext(uri_owl_unionOf,X4,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3216,axiom,
    ( ~ iext(uri_owl_unionOf,X0,sK20)
    | icext(X0,X1) ) ).

cnf(u3236,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_owl_intersectionOf,X4,X1)
    | icext(X4,X3)
    | ~ icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3256,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_intersectionOf,X4,X1)
    | icext(X4,X3)
    | ~ icext(X2,X3)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3264,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK20)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,X1,X3)
    | icext(X3,X2)
    | ~ icext(X0,X2) ) ).

cnf(u3269,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK18)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,X1,X3)
    | icext(X3,X2)
    | ~ icext(X0,X2) ) ).

cnf(u3276,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK20)
    | ~ iext(uri_owl_unionOf,X0,X1)
    | ~ iext(uri_rdf_first,X1,X3)
    | ~ icext(X3,X2)
    | icext(X0,X2) ) ).

cnf(u3281,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK18)
    | ~ iext(uri_owl_unionOf,X0,X1)
    | ~ iext(uri_rdf_first,X1,X3)
    | ~ icext(X3,X2)
    | icext(X0,X2) ) ).

cnf(u3314,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasCousin,sK18) ).

cnf(u3327,axiom,
    icext(uri_ex_hasCousin,sK2(sK4(uri_rdfs_Datatype),uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3331,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_XMLLiteral,sK18) ).

cnf(u3336,axiom,
    icext(uri_ex_hasCousin,sK2(uri_rdf_XMLLiteral,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3345,axiom,
    icext(uri_ex_hasCousin,sK2(uri_rdfs_Seq,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3350,axiom,
    iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),uri_rdfs_member) ).

cnf(u3362,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Bag,sK18) ).

cnf(u3367,axiom,
    icext(uri_ex_hasCousin,sK2(uri_rdf_Bag,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3371,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Alt,sK18) ).

cnf(u3376,axiom,
    icext(uri_ex_hasCousin,sK2(uri_rdf_Alt,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3380,axiom,
    ~ iext(uri_owl_intersectionOf,uri_owl_Ontology,sK18) ).

cnf(u3385,axiom,
    icext(uri_ex_hasCousin,sK2(uri_owl_Ontology,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3390,axiom,
    ioxp(sK2(uri_owl_OntologyProperty,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3407,axiom,
    iext(uri_owl_intersectionOf,uri_owl_DatatypeProperty,sK18) ).

cnf(u3411,axiom,
    icext(uri_ex_hasCousin,sK2(uri_owl_DatatypeProperty,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3420,axiom,
    icext(uri_ex_hasCousin,sK2(uri_owl_AnnotationProperty,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3429,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Datatype,sK18) ).

cnf(u3433,axiom,
    icext(uri_ex_hasCousin,sK2(uri_rdfs_Datatype,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3442,axiom,
    icext(uri_ex_hasCousin,sK2(uri_owl_Nothing,uri_ex_hasCousin,uri_ex_hasFather)) ).

cnf(u3594,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasUncle,sK20) ).

cnf(u3607,axiom,
    icext(uri_ex_hasUncle,sK2(sK4(uri_rdfs_Datatype),uri_ex_hasUncle,sK22)) ).

cnf(u3611,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_XMLLiteral,sK20) ).

cnf(u3616,axiom,
    icext(uri_ex_hasUncle,sK2(uri_rdf_XMLLiteral,uri_ex_hasUncle,sK22)) ).

cnf(u3625,axiom,
    icext(uri_ex_hasUncle,sK2(uri_rdfs_Seq,uri_ex_hasUncle,sK22)) ).

cnf(u3630,axiom,
    iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),uri_rdfs_member) ).

cnf(u3642,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Bag,sK20) ).

cnf(u3647,axiom,
    icext(uri_ex_hasUncle,sK2(uri_rdf_Bag,uri_ex_hasUncle,sK22)) ).

cnf(u3651,axiom,
    ~ iext(uri_owl_intersectionOf,uri_rdf_Alt,sK20) ).

cnf(u3656,axiom,
    icext(uri_ex_hasUncle,sK2(uri_rdf_Alt,uri_ex_hasUncle,sK22)) ).

cnf(u3660,axiom,
    ~ iext(uri_owl_intersectionOf,uri_owl_Ontology,sK20) ).

cnf(u3665,axiom,
    icext(uri_ex_hasUncle,sK2(uri_owl_Ontology,uri_ex_hasUncle,sK22)) ).

cnf(u3670,axiom,
    ioxp(sK2(uri_owl_OntologyProperty,uri_ex_hasUncle,sK22)) ).

cnf(u3691,axiom,
    icext(uri_ex_hasUncle,sK2(uri_owl_DatatypeProperty,uri_ex_hasUncle,sK22)) ).

cnf(u3700,axiom,
    icext(uri_ex_hasUncle,sK2(uri_owl_AnnotationProperty,uri_ex_hasUncle,sK22)) ).

cnf(u3713,axiom,
    icext(uri_ex_hasUncle,sK2(uri_rdfs_Datatype,uri_ex_hasUncle,sK22)) ).

cnf(u3722,axiom,
    icext(uri_ex_hasUncle,sK2(uri_owl_Nothing,uri_ex_hasUncle,sK22)) ).

cnf(u3894,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | icext(X6,X5)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3899,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK18)
    | icext(X0,X1)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_owl_unionOf,X0,X2) ) ).

cnf(u3904,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | icext(X6,X5)
    | ~ iext(uri_owl_unionOf,X6,X3)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u3909,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK20)
    | icext(X0,X1)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ iext(uri_owl_unionOf,X0,X2) ) ).

cnf(u3960,axiom,
    iext(uri_owl_unionOf,uri_owl_DatatypeProperty,sK20) ).

cnf(u3969,axiom,
    iext(uri_owl_unionOf,uri_owl_DatatypeProperty,sK18) ).

cnf(u3978,axiom,
    iext(uri_owl_unionOf,uri_owl_DatatypeProperty,sK21) ).

cnf(u3987,axiom,
    iext(uri_owl_unionOf,uri_owl_DatatypeProperty,sK19) ).

cnf(u4009,axiom,
    iext(uri_owl_intersectionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).

cnf(u4021,axiom,
    icext(uri_owl_DatatypeProperty,X1) ).

cnf(u4138,axiom,
    icext(uri_rdfs_Datatype,X0) ).

cnf(u4388,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_owl_intersectionOf,X6,X3)
    | icext(X6,X5)
    | ~ icext(X4,X5)
    | ~ icext(X2,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X1,X2) ) ).

cnf(u4394,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK20)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,X1,X3)
    | ~ icext(X3,X2)
    | icext(X0,X2) ) ).

cnf(u3101,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK7(X0,X2,X4,X6))
    | ~ icext(X0,sK7(X0,X2,X4,X6))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u248,axiom,
    ( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
    | ~ icext(X0,X1) ) ).

cnf(u1940,axiom,
    iext(uri_rdfs_subPropertyOf,sK4(uri_owl_OntologyProperty),X0) ).

cnf(u1788,axiom,
    ( icext(uri_rdf_List,sK9(uri_rdf_rest,X0))
    | iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).

cnf(u1567,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ) ).

cnf(u1938,axiom,
    ( iext(uri_rdfs_subPropertyOf,sK13(uri_owl_OntologyProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ) ).

cnf(u1786,axiom,
    ( icext(uri_rdf_List,sK9(uri_rdf_first,X0))
    | iext(uri_rdfs_domain,uri_rdf_first,X0) ) ).

cnf(u406,axiom,
    iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).

cnf(u3229,axiom,
    iext(uri_owl_unionOf,sK22,sK18) ).

cnf(u2066,axiom,
    ( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
    | iext(X1,X2,sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
    | ~ icext(sK11(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).

cnf(u3107,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Resource,sK19) ).

cnf(u4398,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK18)
    | ~ iext(uri_rdf_first,sK18,X1)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | icext(X3,sK3(X4,X3,X1,X0))
    | icext(X4,sK3(X4,X3,X1,X0))
    | iext(uri_owl_intersectionOf,X4,X2) ) ).

cnf(u4144,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Datatype,sK19) ).

cnf(u3862,axiom,
    ( iext(uri_rdfs_member,sK14(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0),sK15(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0))
    | iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0) ) ).

cnf(u1570,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).

cnf(u2868,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK2(X3,X2,X0))
    | icext(X3,sK2(X3,X2,X0))
    | iext(uri_owl_intersectionOf,X3,X1) ) ).

cnf(u1587,axiom,
    iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).

cnf(u3220,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,sK18,X1)
    | ~ icext(X2,sK6(X2,X1,X0))
    | iext(uri_owl_unionOf,X2,sK18) ) ).

cnf(u1819,axiom,
    iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Restriction) ).

cnf(u2873,axiom,
    iext(uri_rdfs_range,X0,uri_ex_hasFather) ).

cnf(u3866,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Class,sK20) ).

cnf(u1825,axiom,
    iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Restriction) ).

cnf(u1700,axiom,
    ( ~ icext(X1,sK13(X0,X1))
    | iext(uri_rdfs_subClassOf,X0,X1) ) ).

cnf(u4150,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ).

cnf(u293,axiom,
    ( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
    | ioap(X0) ) ).

cnf(u3224,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Class,sK18) ).

cnf(u423,axiom,
    iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).

cnf(u1698,axiom,
    ( ~ iext(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1,X2)
    | iext(uri_rdfs_member,X1,X2)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u1715,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u1947,axiom,
    ( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
    | iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).

cnf(u1704,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).

cnf(u2622,axiom,
    iext(uri_rdfs_domain,sK1(uri_owl_OntologyProperty,sK22),X0) ).

cnf(u306,axiom,
    ( iext(uri_rdf_type,X0,uri_rdf_Property)
    | ~ ip(X0) ) ).

cnf(u3259,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK20)
    | ~ icext(X0,X2)
    | icext(X3,X2)
    | ~ iext(uri_rdf_first,X1,X4)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,sK20,X3) ) ).

cnf(u2104,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK1(X0,X2))
    | icext(X0,sK1(X0,X2))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u1466,axiom,
    ( ~ iext(uri_rdf__1,X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u4276,axiom,
    icext(uri_ex_hasUncle,X0) ).

cnf(u1861,axiom,
    ( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
    | icext(sK12(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).

cnf(u2874,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_ex_hasFather) ).

cnf(u1859,axiom,
    ( ~ iext(sK11(uri_rdfs_range,X0),X2,X1)
    | icext(sK12(uri_rdfs_range,X0),X1)
    | iext(uri_rdfs_range,uri_rdfs_range,X0) ) ).

cnf(u1865,axiom,
    ( iext(uri_rdfs_member,sK11(uri_rdf__2,X0),sK12(uri_rdf__2,X0))
    | iext(uri_rdfs_range,uri_rdf__2,X0) ) ).

cnf(u4284,axiom,
    iext(uri_owl_unionOf,uri_ex_hasUncle,sK18) ).

cnf(u1879,axiom,
    ( ~ iext(sK4(uri_owl_OntologyProperty),X2,X1)
    | icext(X0,X1) ) ).

cnf(u3002,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | icext(X0,X1) ) ).

cnf(u833,axiom,
    iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

cnf(u4147,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Datatype,sK20) ).

cnf(u4224,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK2(sK12(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),sK18) ) ).

cnf(u323,axiom,
    ( ~ iext(uri_owl_hasValue,X0,X1)
    | icext(uri_owl_Restriction,X0) ) ).

cnf(u1222,axiom,
    icext(uri_rdf_List,sK19) ).

cnf(u461,axiom,
    iext(uri_rdf_first,sK21,sK22) ).

cnf(u2007,axiom,
    ( icext(sK10(uri_rdfs_subClassOf,X0),sK13(sK9(uri_rdfs_subClassOf,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u372,axiom,
    iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u4289,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasUncle,sK21) ).

cnf(u3566,axiom,
    ( iext(uri_rdfs_member,sK14(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0),sK15(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0))
    | iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ) ).

cnf(u1220,axiom,
    ( ~ iext(uri_rdf_predicate,X0,X1)
    | icext(uri_rdfs_Statement,X0) ) ).

cnf(u344,axiom,
    ( ~ iext(uri_rdfs_range,X0,X1)
    | icext(X1,X3)
    | ~ iext(X0,X2,X3) ) ).

cnf(u1884,axiom,
    iext(uri_rdfs_range,uri_owl_unionOf,uri_rdf_List) ).

cnf(u1224,axiom,
    icext(uri_rdf_List,sK21) ).

cnf(u363,axiom,
    ( ~ iext(uri_owl_someValuesFrom,X0,X2)
    | ~ iext(uri_owl_onProperty,X0,X1)
    | iext(X1,X3,sK17(X1,X2,X3))
    | ~ icext(X0,X3) ) ).

cnf(u716,axiom,
    icext(uri_rdf_List,uri_rdf_nil) ).

cnf(u3089,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ icext(X5,sK7(X5,X4,X2,X0))
    | iext(uri_owl_unionOf,X5,X3) ) ).

cnf(u2012,axiom,
    ( icext(sK12(uri_rdfs_range,X0),sK10(sK11(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_range,X0)
    | iext(uri_rdfs_domain,sK11(uri_rdfs_range,X0),X1) ) ).

cnf(u4218,axiom,
    iext(uri_owl_intersectionOf,uri_rdf_Property,sK18) ).

cnf(u1639,axiom,
    iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).

cnf(u2010,axiom,
    ( icext(sK12(uri_rdfs_domain,X0),sK11(sK11(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_domain,X0)
    | iext(uri_rdfs_range,sK11(uri_rdfs_domain,X0),X1) ) ).

cnf(u361,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | ~ iext(uri_owl_hasValue,X0,X2)
    | iext(X1,X3,X2)
    | ~ icext(X0,X3) ) ).

cnf(u1918,axiom,
    ( icext(uri_owl_Restriction,sK14(uri_owl_onProperty,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).

cnf(u2016,axiom,
    ( icext(sK15(uri_rdfs_domain,X0),sK11(sK14(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
    | iext(uri_rdfs_range,sK14(uri_rdfs_domain,X0),X1) ) ).

cnf(u2418,axiom,
    ( iext(uri_rdfs_member,sK9(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0),sK10(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0))
    | iext(uri_rdfs_domain,sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0) ) ).

cnf(u1796,axiom,
    ( icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,X0))
    | iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).

cnf(u2062,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
    | iext(sK10(uri_owl_onProperty,X0),X2,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
    | icext(sK9(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).

cnf(u4043,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK20)
    | ~ iext(uri_rdf_first,sK20,X1)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ icext(X4,sK7(X4,X3,X1,X0))
    | iext(uri_owl_unionOf,X4,X2) ) ).

cnf(u1661,axiom,
    ( icext(X0,sK13(X0,X1))
    | iext(uri_rdfs_subClassOf,X0,X1) ) ).

cnf(u4290,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasUncle,sK19) ).

cnf(u1794,axiom,
    ( ~ iext(uri_owl_hasValue,sK9(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0)
    | ~ iext(sK10(uri_owl_onProperty,X0),X2,X1)
    | icext(sK9(uri_owl_onProperty,X0),X2) ) ).

cnf(u984,axiom,
    ( ~ iext(sK4(uri_owl_OntologyProperty),X0,X1)
    | ix(X1) ) ).

cnf(u1642,axiom,
    iext(uri_rdfs_domain,X0,uri_rdfs_Literal) ).

cnf(u3868,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Resource,sK20) ).

cnf(u1800,axiom,
    ( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
    | icext(sK10(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).

cnf(u3863,axiom,
    ( ~ iext(uri_rdf_first,sK20,X0)
    | ~ icext(X1,sK6(X1,X0,sK22))
    | iext(uri_owl_unionOf,X1,sK20) ) ).

cnf(u1924,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,sK15(uri_rdfs_subPropertyOf,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),X1) ) ).

cnf(u2059,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
    | ~ iext(sK10(uri_owl_onProperty,X0),X2,X3)
    | icext(X1,X3)
    | ~ icext(sK9(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).

cnf(u3872,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK6(sK12(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),sK20) ) ).

cnf(u1789,axiom,
    ( icext(uri_rdf_List,sK10(uri_owl_unionOf,X0))
    | iext(uri_rdfs_domain,uri_owl_unionOf,X0) ) ).

cnf(u1922,axiom,
    ( ~ iext(uri_rdfs_subClassOf,sK15(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u1787,axiom,
    ( icext(uri_rdf_List,sK10(uri_rdf_rest,X0))
    | iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).

cnf(u390,axiom,
    iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).

cnf(u3071,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK3(X0,X2,X4,X6))
    | icext(X0,sK3(X0,X2,X4,X6))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u1665,axiom,
    iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).

cnf(u3468,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ) ).

cnf(u1805,axiom,
    ( iext(uri_rdfs_member,sK9(uri_rdf__3,X0),sK10(uri_rdf__3,X0))
    | iext(uri_rdfs_domain,uri_rdf__3,X0) ) ).

cnf(u3080,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,sK20)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK20,X2) ) ).

cnf(u4088,axiom,
    iext(uri_owl_unionOf,uri_ex_hasCousin,sK18) ).

cnf(u1571,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).

cnf(u388,axiom,
    ( ~ iext(uri_rdf_type,X0,X1)
    | icext(X1,X0) ) ).

cnf(u1803,axiom,
    ( iext(uri_rdfs_member,sK9(uri_rdf__1,X0),sK10(uri_rdf__1,X0))
    | iext(uri_rdfs_domain,uri_rdf__1,X0) ) ).

cnf(u3472,axiom,
    iext(uri_rdfs_subPropertyOf,sK2(uri_owl_OntologyProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ).

cnf(u3111,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK5(sK12(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),sK19) ) ).

cnf(u1577,axiom,
    ( ~ icext(X0,sK0(X0))
    | ~ ic(X0)
    | iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).

cnf(u2063,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
    | iext(sK12(uri_owl_onProperty,X0),X2,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
    | icext(sK11(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).

cnf(u1809,axiom,
    ( icext(uri_rdfs_Statement,sK9(uri_rdf_predicate,X0))
    | iext(uri_rdfs_domain,uri_rdf_predicate,X0) ) ).

cnf(u407,axiom,
    iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1931,axiom,
    ( iext(uri_rdfs_seeAlso,sK14(uri_rdfs_isDefinedBy,X0),sK15(uri_rdfs_isDefinedBy,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).

cnf(u3104,axiom,
    iext(uri_owl_unionOf,uri_owl_Thing,sK19) ).

cnf(u4399,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK20)
    | ~ iext(uri_rdf_first,sK20,X1)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | icext(X3,sK3(X4,X3,X1,X0))
    | icext(X4,sK3(X4,X3,X1,X0))
    | iext(uri_owl_intersectionOf,X4,X2) ) ).

cnf(u1937,axiom,
    ( iext(uri_rdfs_member,sK14(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK15(sK4(uri_rdfs_ContainerMembershipProperty),X0))
    | iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).

cnf(u3228,axiom,
    iext(uri_owl_unionOf,uri_ex_hasFather,sK18) ).

cnf(u1845,axiom,
    ( icext(sK12(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | icext(sK11(uri_owl_complementOf,X0),X1) ) ).

cnf(u1843,axiom,
    ( iext(X0,sK11(X0,X1),sK12(X0,X1))
    | iext(uri_rdfs_range,X0,X1) ) ).

cnf(u2781,axiom,
    ( iext(uri_rdfs_member,sK9(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0),sK10(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0))
    | iext(uri_rdfs_domain,sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0) ) ).

cnf(u4285,axiom,
    iext(uri_owl_unionOf,uri_ex_hasUncle,sK20) ).

cnf(u3232,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK6(sK10(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),sK18) ) ).

cnf(u1849,axiom,
    ( icext(uri_rdf_List,sK11(uri_rdf_rest,X0))
    | iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).

cnf(u317,axiom,
    ( ~ iext(uri_owl_allValuesFrom,X0,X1)
    | icext(uri_owl_Restriction,X0) ) ).

cnf(u3751,axiom,
    iext(uri_rdfs_range,sK2(uri_owl_OntologyProperty,uri_ex_hasUncle,sK22),X0) ).

cnf(u3287,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK1(sK15(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),sK21) ) ).

cnf(u4155,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u831,axiom,
    iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).

cnf(u1977,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK9(X1,sK15(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_rdfs_domain,X1,sK15(uri_owl_complementOf,X0)) ) ).

cnf(u1863,axiom,
    ( iext(sK12(uri_rdfs_subPropertyOf,X0),X1,X2)
    | iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
    | ~ iext(sK11(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).

cnf(u4153,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Datatype,uri_rdf_nil) ).

cnf(u4283,axiom,
    iext(uri_owl_unionOf,uri_ex_hasUncle,sK21) ).

cnf(u3912,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,sK18,X1)
    | ~ icext(X1,sK2(X2,X1,X0))
    | ~ icext(X2,sK2(X2,X1,X0))
    | iext(uri_owl_intersectionOf,X2,sK18) ) ).

cnf(u358,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | ~ iext(uri_owl_allValuesFrom,X0,X2)
    | iext(X1,X3,sK16(X1,X2,X3))
    | icext(X0,X3) ) ).

cnf(u2618,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0) ) ).

cnf(u4281,axiom,
    ( ~ icext(X0,sK2(X0,uri_ex_hasUncle,sK22))
    | iext(uri_owl_intersectionOf,X0,sK20) ) ).

cnf(u846,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
    | icext(X0,X1) ) ).

cnf(u1973,axiom,
    ( ~ icext(sK14(uri_owl_complementOf,X0),sK13(sK15(uri_owl_complementOf,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,sK15(uri_owl_complementOf,X0),X1) ) ).

cnf(u3090,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ icext(X5,sK7(X5,X4,X2,X0))
    | iext(uri_owl_unionOf,X5,X3) ) ).

cnf(u1862,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,sK12(uri_rdfs_subPropertyOf,X0),X1)
    | iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_subPropertyOf,X0),X1) ) ).

cnf(u458,axiom,
    iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave) ).

cnf(u1868,axiom,
    ( icext(uri_rdfs_Statement,sK11(uri_rdf_subject,X0))
    | iext(uri_rdfs_range,uri_rdf_subject,X0) ) ).

cnf(u2624,axiom,
    iext(uri_rdfs_subPropertyOf,sK1(uri_owl_OntologyProperty,sK22),X0) ).

cnf(u1866,axiom,
    ( iext(uri_rdfs_member,sK11(uri_rdf__3,X0),sK12(uri_rdf__3,X0))
    | iext(uri_rdfs_range,uri_rdf__3,X0) ) ).

cnf(u373,axiom,
    iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).

cnf(u334,axiom,
    ( ~ iext(uri_owl_unionOf,X0,X1)
    | icext(uri_rdf_List,X1) ) ).

cnf(u456,axiom,
    iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly) ).

cnf(u4033,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty) ).

cnf(u1994,axiom,
    ( icext(sK15(uri_rdfs_subClassOf,X0),sK13(sK14(uri_rdfs_subClassOf,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK14(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u1902,axiom,
    ( icext(sK12(uri_rdfs_subClassOf,X0),sK13(sK11(uri_rdfs_subClassOf,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK11(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u368,axiom,
    iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

cnf(u462,axiom,
    iext(uri_rdf_rest,sK20,sK21) ).

cnf(u2783,axiom,
    ( iext(uri_rdfs_member,sK14(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0),sK15(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0))
    | iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0) ) ).

cnf(u1908,axiom,
    ( icext(uri_rdf_List,sK15(uri_owl_intersectionOf,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X0) ) ).

cnf(u2260,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ icext(uri_ex_hasFather,X1)
    | icext(X0,X1) ) ).

cnf(u1906,axiom,
    ( ~ icext(sK15(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | ~ icext(sK14(uri_owl_complementOf,X0),X1) ) ).

cnf(u3152,axiom,
    ( ~ icext(X0,sK5(X0,sK22))
    | iext(uri_owl_unionOf,X0,sK21) ) ).

cnf(u4089,axiom,
    iext(uri_owl_unionOf,uri_ex_hasCousin,sK20) ).

cnf(u2030,axiom,
    ( icext(sK10(uri_rdfs_range,X0),sK10(sK9(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_range,X0)
    | iext(uri_rdfs_domain,sK9(uri_rdfs_range,X0),X1) ) ).

cnf(u4085,axiom,
    ( ~ icext(X0,sK2(X0,uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_owl_intersectionOf,X0,sK18) ) ).

cnf(u1912,axiom,
    ( icext(uri_rdf_List,sK15(uri_owl_unionOf,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,X0) ) ).

cnf(u1649,axiom,
    ( ~ icext(X1,sK12(X0,X1))
    | iext(uri_rdfs_range,X0,X1) ) ).

cnf(u3036,axiom,
    iext(uri_owl_intersectionOf,sK22,uri_rdf_nil) ).

cnf(u3445,axiom,
    ( ~ iext(uri_rdf_first,sK18,X1)
    | icext(X1,X0)
    | ~ icext(uri_ex_hasCousin,X0) ) ).

cnf(u257,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,X5)
    | icext(X2,X5)
    | ~ icext(X0,X5)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u479,axiom,
    icext(uri_owl_Thing,X0) ).

cnf(u2284,axiom,
    ( ~ iext(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u2419,axiom,
    ( iext(uri_rdfs_member,sK11(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0),sK12(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0))
    | iext(uri_rdfs_range,sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0) ) ).

cnf(u1662,axiom,
    iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).

cnf(u1917,axiom,
    ( ~ iext(uri_owl_hasValue,sK14(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
    | ~ iext(sK15(uri_owl_onProperty,X0),X2,X1)
    | icext(sK14(uri_owl_onProperty,X0),X2) ) ).

cnf(u1791,axiom,
    ( icext(uri_owl_Restriction,sK9(uri_owl_allValuesFrom,X0))
    | iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ) ).

cnf(u2057,axiom,
    ( ~ iext(uri_owl_unionOf,X2,sK19)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK19,X0) ) ).

cnf(u3102,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ icext(X1,sK5(X1,X0))
    | iext(uri_owl_unionOf,X1,sK19) ) ).

cnf(u1915,axiom,
    ( icext(uri_owl_Restriction,sK14(uri_owl_hasValue,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ) ).

cnf(u1790,axiom,
    ( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
    | iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).

cnf(u3095,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,sK7(X0,X2,X4,X6))
    | ~ icext(X0,sK7(X0,X2,X4,X6))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u1793,axiom,
    ( ~ iext(uri_owl_hasValue,sK9(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0)
    | iext(sK10(uri_owl_onProperty,X0),X2,X1)
    | ~ icext(sK9(uri_owl_onProperty,X0),X2) ) ).

cnf(u1668,axiom,
    iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ).

cnf(u4086,axiom,
    iext(uri_owl_unionOf,uri_ex_hasCousin,sK19) ).

cnf(u1807,axiom,
    ( icext(uri_rdfs_Statement,sK9(uri_rdf_subject,X0))
    | iext(uri_rdfs_domain,uri_rdf_subject,X0) ) ).

cnf(u2058,axiom,
    ( ~ iext(uri_owl_unionOf,X2,sK21)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK21,X0) ) ).

cnf(u4090,axiom,
    iext(uri_rdfs_domain,X0,uri_ex_hasCousin) ).

cnf(u3230,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK6(sK12(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),sK18) ) ).

cnf(u4092,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_ex_hasCousin) ).

cnf(u3469,axiom,
    ( ~ iext(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u1672,axiom,
    iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0) ).

cnf(u3223,axiom,
    iext(uri_owl_unionOf,uri_owl_Thing,sK18) ).

cnf(u1026,axiom,
    ~ icext(uri_owl_Ontology,X0) ).

cnf(u1921,axiom,
    ( ~ iext(sK14(uri_rdfs_range,X0),X2,X1)
    | icext(sK15(uri_rdfs_range,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0) ) ).

cnf(u4249,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,sK20,X1)
    | ~ icext(X1,sK2(X2,X1,X0))
    | ~ icext(X2,sK2(X2,X1,X0))
    | iext(uri_owl_intersectionOf,X2,sK20) ) ).

cnf(u3225,axiom,
    iext(uri_owl_unionOf,uri_rdf_Property,sK18) ).

cnf(u3227,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Literal,sK18) ).

cnf(u1702,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).

cnf(u3226,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Resource,sK18) ).

cnf(u301,axiom,
    ( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
    | ioxp(X0) ) ).

cnf(u431,axiom,
    iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement) ).

cnf(u918,axiom,
    iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).

cnf(u2848,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | icext(X0,X1) ) ).

cnf(u4286,axiom,
    iext(uri_rdfs_domain,X0,uri_ex_hasUncle) ).

cnf(u429,axiom,
    iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) ).

cnf(u4403,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK18)
    | ~ iext(uri_rdf_first,sK18,X1)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ icext(X3,sK3(X4,X3,X1,X0))
    | ~ icext(X4,sK3(X4,X3,X1,X0))
    | iext(uri_owl_intersectionOf,X4,X2) ) ).

cnf(u1468,axiom,
    ( ~ iext(uri_rdf__3,X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u1846,axiom,
    ( icext(uri_rdf_List,sK12(uri_owl_intersectionOf,X0))
    | iext(uri_rdfs_range,uri_owl_intersectionOf,X0) ) ).

cnf(u4214,axiom,
    iext(uri_owl_intersectionOf,uri_owl_Thing,sK18) ).

cnf(u1852,axiom,
    ( icext(uri_owl_Restriction,sK11(uri_owl_allValuesFrom,X0))
    | iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ) ).

cnf(u1203,axiom,
    ( ~ iext(uri_rdf_rest,X0,X1)
    | icext(uri_rdf_List,X0) ) ).

cnf(u1850,axiom,
    ( icext(uri_rdf_List,sK12(uri_owl_unionOf,X0))
    | iext(uri_rdfs_range,uri_owl_unionOf,X0) ) ).

cnf(u1974,axiom,
    ( ~ icext(sK14(uri_owl_complementOf,X0),sK4(sK15(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u4271,axiom,
    ( ~ iext(uri_rdf_first,sK20,X1)
    | icext(X1,X0) ) ).

cnf(u3013,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,sK6(X0,X2,X4))
    | icext(X2,sK6(X0,X2,X4))
    | icext(X0,sK6(X0,X2,X4))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u4031,axiom,
    iext(uri_rdfs_domain,X0,uri_owl_DatatypeProperty) ).

cnf(u1978,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK12(X1,sK15(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_rdfs_range,X1,sK15(uri_owl_complementOf,X0)) ) ).

cnf(u446,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
    | ~ iext(uri_rdfs_subPropertyOf,X1,X2)
    | iext(uri_rdfs_subPropertyOf,X0,X2) ) ).

cnf(u1856,axiom,
    ( icext(uri_owl_Restriction,sK11(uri_owl_onProperty,X0))
    | iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).

cnf(u1223,axiom,
    icext(uri_rdf_List,sK20) ).

cnf(u4297,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_ex_hasUncle,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u3157,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Literal,sK21) ).

cnf(u357,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | ~ iext(uri_owl_allValuesFrom,X0,X2)
    | ~ iext(X1,X3,X4)
    | icext(X2,X4)
    | ~ icext(X0,X3) ) ).

cnf(u329,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | icext(uri_owl_Restriction,X0) ) ).

cnf(u459,axiom,
    iext(uri_owl_inverseOf,sK22,uri_ex_hasFather) ).

cnf(u3161,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK5(sK15(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),sK21) ) ).

cnf(u1892,axiom,
    ( ~ icext(sK11(uri_owl_complementOf,X0),sK13(sK12(uri_owl_complementOf,X0),X1))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,sK12(uri_owl_complementOf,X0),X1) ) ).

cnf(u3158,axiom,
    iext(uri_owl_unionOf,uri_ex_hasFather,sK21) ).

cnf(u1629,axiom,
    ic(X0) ).

cnf(u3086,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X6,sK7(X0,X2,X4,X6))
    | ~ icext(X0,sK7(X0,X2,X4,X6))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u457,axiom,
    iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob) ).

cnf(u724,axiom,
    icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).

cnf(u2014,axiom,
    ( icext(sK12(uri_rdfs_range,X0),sK15(sK11(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_range,X0)
    | iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_range,X0),X1) ) ).

cnf(u1896,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK9(X1,sK12(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_rdfs_domain,X1,sK12(uri_owl_complementOf,X0)) ) ).

cnf(u4287,axiom,
    iext(uri_rdfs_range,X0,uri_ex_hasUncle) ).

cnf(u3162,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK5(sK10(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),sK21) ) ).

cnf(u3289,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,sK18,X1)
    | icext(X1,sK2(X2,X1,X0))
    | icext(X2,sK2(X2,X1,X0))
    | iext(uri_owl_intersectionOf,X2,sK18) ) ).

cnf(u2020,axiom,
    ( icext(sK15(uri_rdfs_range,X0),sK15(sK14(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
    | iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_range,X0),X1) ) ).

cnf(u3286,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK1(sK12(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),sK21) ) ).

cnf(u2018,axiom,
    ( icext(sK15(uri_rdfs_range,X0),sK10(sK14(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
    | iext(uri_rdfs_domain,sK14(uri_rdfs_range,X0),X1) ) ).

cnf(u369,axiom,
    iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).

cnf(u463,axiom,
    iext(uri_rdf_first,sK20,uri_ex_hasUncle) ).

cnf(u4353,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Literal,sK20) ).

cnf(u3290,axiom,
    ( ~ iext(uri_rdf_first,sK18,X0)
    | icext(X0,sK2(X1,X0,uri_ex_hasFather))
    | icext(X1,sK2(X1,X0,uri_ex_hasFather))
    | iext(uri_owl_intersectionOf,X1,sK18) ) ).

cnf(u1652,axiom,
    iext(uri_rdfs_range,X0,uri_rdf_Property) ).

cnf(u2283,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0) ) ).

cnf(u229,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,X5)
    | ~ icext(X2,X5)
    | icext(X0,X5)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u497,axiom,
    iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u1121,axiom,
    ~ icext(uri_rdf_Alt,X0) ).

cnf(u1847,axiom,
    ( icext(uri_rdf_List,sK11(uri_rdf_first,X0))
    | iext(uri_rdfs_range,uri_rdf_first,X0) ) ).

cnf(u4359,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK2(sK15(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),sK20) ) ).

cnf(u2068,axiom,
    ( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK10(uri_owl_someValuesFrom,X0),X2)
    | ~ iext(X1,X3,X2)
    | icext(sK9(uri_owl_someValuesFrom,X0),X3)
    | iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).

cnf(u1905,axiom,
    ( iext(X0,sK14(X0,X1),sK15(X0,X1))
    | iext(uri_rdfs_subPropertyOf,X0,X1) ) ).

cnf(u1669,axiom,
    iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0) ).

cnf(u2029,axiom,
    ( icext(sK10(uri_rdfs_domain,X0),sK14(sK9(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_domain,X0)
    | iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_domain,X0),X1) ) ).

cnf(u1919,axiom,
    ( icext(uri_owl_Restriction,sK14(uri_owl_someValuesFrom,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).

cnf(u268,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,X7)
    | icext(X0,X7)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u1667,axiom,
    ( ioxp(sK13(uri_owl_OntologyProperty,X0))
    | iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ) ).

cnf(u2027,axiom,
    ( icext(sK10(uri_rdfs_domain,X0),sK9(sK9(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_domain,X0)
    | iext(uri_rdfs_domain,sK9(uri_rdfs_domain,X0),X1) ) ).

cnf(u4357,axiom,
    iext(uri_owl_intersectionOf,sK22,sK20) ).

cnf(u1784,axiom,
    ( icext(sK10(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | icext(sK9(uri_owl_complementOf,X0),X1) ) ).

cnf(u2065,axiom,
    ( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
    | iext(X1,X2,sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
    | ~ icext(sK9(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).

cnf(u2287,axiom,
    iext(uri_rdfs_domain,sK1(uri_owl_OntologyProperty,uri_ex_hasFather),X0) ).

cnf(u1138,axiom,
    ~ icext(uri_rdf_Bag,X0) ).

cnf(u1813,axiom,
    ( iext(uri_rdfs_domain,sK13(uri_owl_OntologyProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ) ).

cnf(u4080,axiom,
    ( ~ iext(uri_rdf_first,sK18,X1)
    | icext(X1,X0) ) ).

cnf(u258,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,X5)
    | icext(X0,X5)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u396,axiom,
    ( ~ icext(uri_rdfs_ContainerMembershipProperty,X0)
    | iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member) ) ).

cnf(u3870,axiom,
    iext(uri_owl_unionOf,uri_ex_hasFather,sK20) ).

cnf(u2597,axiom,
    ~ iext(sK1(uri_owl_OntologyProperty,sK22),X0,X1) ).

cnf(u2056,axiom,
    ( ~ iext(uri_owl_unionOf,X2,sK21)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK21,X0) ) ).

cnf(u1817,axiom,
    ( ~ iext(sK4(uri_owl_OntologyProperty),X1,X2)
    | icext(X0,X1) ) ).

cnf(u3874,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK6(sK10(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),sK20) ) ).

cnf(u1939,axiom,
    ( iext(uri_rdfs_member,sK14(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK15(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
    | iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u4355,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasCousin,sK20) ).

cnf(u3725,axiom,
    ( ~ iext(uri_rdf_first,sK20,X1)
    | icext(X1,X0)
    | ~ icext(uri_ex_hasUncle,X0) ) ).

cnf(u4360,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK2(sK10(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),sK20) ) ).

cnf(u1945,axiom,
    ( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
    | iext(uri_rdfs_subPropertyOf,X0,X1) ) ).

cnf(u4140,axiom,
    idc(X0) ).

cnf(u298,axiom,
    ( ~ ioxp(X0)
    | ~ iext(X0,X1,X2)
    | ix(X2) ) ).

cnf(u4251,axiom,
    ( ~ icext(uri_ex_hasUncle,sK2(X0,uri_ex_hasUncle,sK22))
    | ~ icext(X0,sK2(X0,uri_ex_hasUncle,sK22))
    | iext(uri_owl_intersectionOf,X0,sK20) ) ).

cnf(u2869,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK2(X3,X2,X0))
    | icext(X3,sK2(X3,X2,X0))
    | iext(uri_owl_intersectionOf,X3,X1) ) ).

cnf(u3869,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Literal,sK20) ).

cnf(u3465,axiom,
    ~ iext(sK2(uri_owl_OntologyProperty,uri_ex_hasCousin,uri_ex_hasFather),X0,X1) ).

cnf(u2867,axiom,
    icext(uri_ex_hasFather,X0) ).

cnf(u3867,axiom,
    iext(uri_owl_unionOf,uri_rdf_Property,sK20) ).

cnf(u1928,axiom,
    ( iext(uri_rdfs_member,sK14(uri_rdf__3,X0),sK15(uri_rdf__3,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ) ).

cnf(u3873,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK6(sK15(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),sK20) ) ).

cnf(u2592,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ icext(sK22,X1)
    | icext(X0,X1) ) ).

cnf(u315,axiom,
    ( iext(uri_rdf_type,X0,uri_rdfs_Literal)
    | ~ lv(X0) ) ).

cnf(u2623,axiom,
    iext(uri_rdfs_range,sK1(uri_owl_OntologyProperty,sK22),X0) ).

cnf(u1469,axiom,
    ( ~ iext(uri_rdfs_isDefinedBy,X0,X1)
    | iext(uri_rdfs_seeAlso,X0,X1) ) ).

cnf(u4266,axiom,
    iext(uri_owl_intersectionOf,uri_owl_DatatypeProperty,sK20) ).

cnf(u1212,axiom,
    ( ~ iext(uri_rdf_object,X0,X1)
    | icext(uri_rdfs_Statement,X0) ) ).

cnf(u4219,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Resource,sK18) ).

cnf(u2619,axiom,
    ( ~ iext(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u1705,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).

cnf(u3141,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ icext(X2,sK3(X5,X4,X2,X0))
    | ~ icext(X4,sK3(X5,X4,X2,X0))
    | ~ icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u4220,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Literal,sK18) ).

cnf(u3082,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | icext(X4,sK3(X5,X4,X2,X0))
    | icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u1870,axiom,
    ( icext(uri_rdfs_Statement,sK11(uri_rdf_predicate,X0))
    | iext(uri_rdfs_range,uri_rdf_predicate,X0) ) ).

cnf(u2998,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK2(X3,X2,X0))
    | ~ icext(X3,sK2(X3,X2,X0))
    | iext(uri_owl_intersectionOf,X3,X1) ) ).

cnf(u1473,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0)
    | iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).

cnf(u1876,axiom,
    ( iext(uri_rdfs_member,sK11(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK12(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
    | iext(uri_rdfs_range,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u1874,axiom,
    ( iext(uri_rdfs_member,sK11(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK12(sK4(uri_rdfs_ContainerMembershipProperty),X0))
    | iext(uri_rdfs_range,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).

cnf(u4225,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK2(sK15(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),sK18) ) ).

cnf(u1998,axiom,
    ( ~ icext(sK9(uri_owl_complementOf,X0),sK4(sK10(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u4053,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u1617,axiom,
    icext(uri_rdfs_Literal,X0) ).

cnf(u1631,axiom,
    icext(uri_rdf_Property,X0) ).

cnf(u2002,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK12(X1,sK10(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_rdfs_range,X1,sK10(uri_owl_complementOf,X0)) ) ).

cnf(u4282,axiom,
    iext(uri_owl_unionOf,uri_ex_hasUncle,sK19) ).

cnf(u3156,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Resource,sK21) ).

cnf(u3023,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X6,sK3(X0,X2,X4,X6))
    | icext(X0,sK3(X0,X2,X4,X6))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u1653,axiom,
    iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).

cnf(u213,axiom,
    ( ~ iext(uri_owl_complementOf,X0,X1)
    | ~ icext(X1,X2)
    | ~ icext(X0,X2) ) ).

cnf(u3160,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK5(sK12(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),sK21) ) ).

cnf(u359,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | ~ iext(uri_owl_allValuesFrom,X0,X2)
    | ~ icext(X2,sK16(X1,X2,X3))
    | icext(X0,X3) ) ).

cnf(u1634,axiom,
    ip(X0) ).

cnf(u481,axiom,
    icext(uri_rdfs_Resource,X0) ).

cnf(u1651,axiom,
    iext(uri_rdfs_range,X0,uri_rdfs_Class) ).

cnf(u468,axiom,
    iext(uri_rdf_first,sK18,uri_ex_hasCousin) ).

cnf(u224,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,X3)
    | ~ icext(X0,X3)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2052,axiom,
    ( ~ iext(uri_owl_intersectionOf,X2,sK21)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK21,X0) ) ).

cnf(u2013,axiom,
    ( icext(sK12(uri_rdfs_range,X0),sK12(sK11(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_range,X0)
    | iext(uri_rdfs_range,sK11(uri_rdfs_range,X0),X1) ) ).

cnf(u3288,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK1(sK10(uri_owl_complementOf,X0),sK22))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),sK21) ) ).

cnf(u1903,axiom,
    ( icext(sK12(uri_rdfs_subClassOf,X0),sK4(sK11(uri_rdfs_subClassOf,X0)))
    | iext(uri_rdfs_range,uri_rdfs_subClassOf,X0)
    | iext(uri_owl_unionOf,sK11(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).

cnf(u2011,axiom,
    ( icext(sK12(uri_rdfs_domain,X0),sK14(sK11(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_domain,X0)
    | iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_domain,X0),X1) ) ).

cnf(u3565,axiom,
    ( iext(uri_rdfs_member,sK11(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0),sK12(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0))
    | iext(uri_rdfs_range,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ) ).

cnf(u3065,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,sK3(X0,X2,X4,X6))
    | icext(X0,sK3(X0,X2,X4,X6))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2017,axiom,
    ( icext(sK15(uri_rdfs_domain,X0),sK14(sK14(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
    | iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_domain,X0),X1) ) ).

cnf(u253,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,X3)
    | icext(X0,X3)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u2031,axiom,
    ( icext(sK10(uri_rdfs_range,X0),sK12(sK9(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_range,X0)
    | iext(uri_rdfs_range,sK9(uri_rdfs_range,X0),X1) ) ).

cnf(u370,axiom,
    iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).

cnf(u3569,axiom,
    ( ~ iext(uri_rdf_first,sK20,X0)
    | icext(X0,sK2(X1,X0,sK22))
    | icext(X1,sK2(X1,X0,sK22))
    | iext(uri_owl_intersectionOf,X1,sK20) ) ).

cnf(u1795,axiom,
    ( icext(uri_owl_Restriction,sK9(uri_owl_onProperty,X0))
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).

cnf(u1670,axiom,
    iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0) ).

cnf(u228,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,X5)
    | ~ icext(X0,X5)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u3155,axiom,
    iext(uri_owl_unionOf,uri_rdf_Property,sK21) ).

cnf(u1801,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,sK10(uri_rdfs_subPropertyOf,X0),X1)
    | iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,X0),X1) ) ).

cnf(u3860,axiom,
    ( iext(uri_rdfs_member,sK9(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0),sK10(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0))
    | iext(uri_rdfs_domain,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0) ) ).

cnf(u3571,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X3,sK6(X3,X2,X0))
    | iext(uri_owl_unionOf,X3,X1) ) ).

cnf(u269,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,X7)
    | icext(X0,X7)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u1815,axiom,
    iext(uri_rdfs_domain,sK4(uri_owl_OntologyProperty),X0) ).

cnf(u3108,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Literal,sK19) ).

cnf(u4097,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_ex_hasCousin,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u1923,axiom,
    ( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
    | icext(sK15(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).

cnf(u3864,axiom,
    ( ~ icext(X0,sK6(X0,uri_ex_hasUncle,sK22))
    | iext(uri_owl_unionOf,X0,sK20) ) ).

cnf(u1929,axiom,
    ( icext(uri_rdfs_Statement,sK14(uri_rdf_object,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ) ).

cnf(u4348,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Class,sK20) ).

cnf(u259,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,X5)
    | icext(X0,X5)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u2069,axiom,
    ( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK12(uri_owl_someValuesFrom,X0),X2)
    | ~ iext(X1,X3,X2)
    | icext(sK11(uri_owl_someValuesFrom,X0),X3)
    | iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).

cnf(u2064,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
    | iext(sK15(uri_owl_onProperty,X0),X2,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
    | icext(sK14(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).

cnf(u1943,axiom,
    ( ~ iext(sK4(uri_owl_OntologyProperty),X1,X2)
    | iext(X0,X1,X2) ) ).

cnf(u3066,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | icext(X2,sK3(X5,X4,X2,X0))
    | icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u3467,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,sK20,X1)
    | icext(X1,sK2(X2,X1,X0))
    | icext(X2,sK2(X2,X1,X0))
    | iext(uri_owl_intersectionOf,X2,sK20) ) ).

cnf(u2853,axiom,
    ( ~ icext(X0,sK1(X0,sK22))
    | ~ icext(sK22,sK1(X0,sK22))
    | iext(uri_owl_intersectionOf,X0,sK21) ) ).

cnf(u1032,axiom,
    ~ icext(uri_owl_AnnotationProperty,X0) ).

cnf(u3727,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,sK20,X1)
    | ~ icext(X2,sK6(X2,X1,X0))
    | iext(uri_owl_unionOf,X2,sK20) ) ).

cnf(u1162,axiom,
    ~ icext(uri_rdfs_Seq,X0) ).

cnf(u387,axiom,
    ( iext(uri_rdf_type,X0,X1)
    | ~ icext(X1,X0) ) ).

cnf(u2070,axiom,
    ( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK15(uri_owl_someValuesFrom,X0),X2)
    | ~ iext(X1,X3,X2)
    | icext(sK14(uri_owl_someValuesFrom,X0),X3)
    | iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).

cnf(u2040,axiom,
    ( ~ iext(sK11(uri_rdfs_subPropertyOf,X0),sK14(X1,sK12(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK12(uri_rdfs_subPropertyOf,X0)))
    | iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,X1,sK12(uri_rdfs_subPropertyOf,X0)) ) ).

cnf(u1650,axiom,
    iext(uri_rdfs_range,X0,uri_owl_Thing) ).

cnf(u2866,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK2(X0,X2,X4))
    | icext(X0,sK2(X0,X2,X4))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u3871,axiom,
    iext(uri_owl_unionOf,sK22,sK20) ).

cnf(u3748,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0) ) ).

cnf(u299,axiom,
    ( ~ ioxp(X0)
    | ~ iext(X0,X1,X2)
    | ix(X1) ) ).

cnf(u2877,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_ex_hasFather,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u2872,axiom,
    iext(uri_rdfs_domain,X0,uri_ex_hasFather) ).

cnf(u286,axiom,
    ( iext(uri_rdf_type,X0,uri_rdfs_Class)
    | ~ ic(X0) ) ).

cnf(u408,axiom,
    iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

cnf(u3746,axiom,
    ~ iext(sK2(uri_owl_OntologyProperty,uri_ex_hasUncle,sK22),X0,X1) ).

cnf(u4145,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Datatype,sK21) ).

cnf(u1948,axiom,
    iext(uri_rdfs_subPropertyOf,X0,X0) ).

cnf(u3752,axiom,
    iext(uri_rdfs_subPropertyOf,sK2(uri_owl_OntologyProperty,uri_ex_hasUncle,sK22),X0) ).

cnf(u3106,axiom,
    iext(uri_owl_unionOf,uri_rdf_Property,sK19) ).

cnf(u1196,axiom,
    ~ icext(sK4(uri_rdfs_Datatype),X0) ).

cnf(u427,axiom,
    iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement) ).

cnf(u1854,axiom,
    ( ~ iext(uri_owl_hasValue,sK11(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_range,uri_owl_onProperty,X0)
    | iext(sK12(uri_owl_onProperty,X0),X2,X1)
    | ~ icext(sK11(uri_owl_onProperty,X0),X2) ) ).

cnf(u4151,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Datatype,sK21) ).

cnf(u2354,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | ~ icext(X0,sK1(X1,X0))
    | ~ icext(X1,sK1(X1,X0))
    | iext(uri_owl_intersectionOf,X1,sK19) ) ).

cnf(u4152,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Datatype,sK19) ).

cnf(u1925,axiom,
    ( iext(sK15(uri_rdfs_subPropertyOf,X0),X1,X2)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
    | ~ iext(sK14(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).

cnf(u1703,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).

cnf(u4149,axiom,
    iext(uri_rdfs_range,X0,uri_rdfs_Datatype) ).

cnf(u1584,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).

cnf(u1860,axiom,
    ( ~ iext(uri_rdfs_subClassOf,sK12(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_range,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK11(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u1708,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_owl_Thing,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u3091,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,sK18)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK18,X2) ) ).

cnf(u4280,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasUncle,sK18) ).

cnf(u1858,axiom,
    ( ~ iext(sK11(uri_rdfs_domain,X0),X1,X2)
    | icext(sK12(uri_rdfs_domain,X0),X1)
    | iext(uri_rdfs_range,uri_rdfs_domain,X0) ) ).

cnf(u3913,axiom,
    ( ~ iext(uri_rdf_first,sK18,X0)
    | ~ icext(X0,sK2(X1,X0,uri_ex_hasFather))
    | ~ icext(X1,sK2(X1,X0,uri_ex_hasFather))
    | iext(uri_owl_intersectionOf,X1,sK18) ) ).

cnf(u1706,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ).

cnf(u3149,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ icext(X1,sK5(X1,X0))
    | iext(uri_owl_unionOf,X1,sK21) ) ).

cnf(u1864,axiom,
    ( iext(uri_rdfs_member,sK11(uri_rdf__1,X0),sK12(uri_rdf__1,X0))
    | iext(uri_rdfs_range,uri_rdf__1,X0) ) ).

cnf(u3258,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,sK20)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK20,X2) ) ).

cnf(u1470,axiom,
    ( ~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u832,axiom,
    iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).

cnf(u3153,axiom,
    iext(uri_owl_unionOf,uri_owl_Thing,sK21) ).

cnf(u2420,axiom,
    ( iext(uri_rdfs_member,sK14(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0),sK15(sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0))
    | iext(uri_rdfs_subPropertyOf,sK1(uri_rdfs_ContainerMembershipProperty,uri_ex_hasFather),X0) ) ).

cnf(u3140,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ icext(X2,sK3(X5,X4,X2,X0))
    | ~ icext(X4,sK3(X5,X4,X2,X0))
    | ~ icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u4226,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK2(sK10(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),sK18) ) ).

cnf(u3564,axiom,
    ( iext(uri_rdfs_member,sK9(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0),sK10(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0))
    | iext(uri_rdfs_domain,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ) ).

cnf(u1729,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u1483,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0)
    | iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).

cnf(u726,axiom,
    icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

cnf(u1637,axiom,
    ( ~ icext(X1,sK9(X0,X1))
    | iext(uri_rdfs_domain,X0,X1) ) ).

cnf(u1869,axiom,
    ( iext(uri_rdfs_seeAlso,sK11(uri_rdfs_isDefinedBy,X0),sK12(uri_rdfs_isDefinedBy,X0))
    | iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ) ).

cnf(u4288,axiom,
    iext(uri_rdfs_subClassOf,X0,uri_ex_hasUncle) ).

cnf(u1743,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdf_Property,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u465,axiom,
    iext(uri_rdf_rest,sK19,uri_rdf_nil) ).

cnf(u376,axiom,
    iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).

cnf(u452,axiom,
    ir(X0) ).

cnf(u1867,axiom,
    ( icext(uri_rdfs_Statement,sK11(uri_rdf_object,X0))
    | iext(uri_rdfs_range,uri_rdf_object,X0) ) ).

cnf(u1624,axiom,
    icext(uri_rdfs_Class,X0) ).

cnf(u3914,axiom,
    ( ~ icext(uri_ex_hasCousin,sK2(X0,uri_ex_hasCousin,uri_ex_hasFather))
    | ~ icext(X0,sK2(X0,uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_owl_intersectionOf,X0,sK18) ) ).

cnf(u4094,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasCousin,sK19) ).

cnf(u3283,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK1(sK12(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),sK19) ) ).

cnf(u3038,axiom,
    ( ~ iext(uri_rdfs_subClassOf,sK22,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u1997,axiom,
    ( ~ icext(sK9(uri_owl_complementOf,X0),sK13(sK10(uri_owl_complementOf,X0),X1))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,sK10(uri_owl_complementOf,X0),X1) ) ).

cnf(u3272,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK18)
    | icext(X0,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,X1,X4)
    | ~ iext(uri_owl_unionOf,X0,X1)
    | ~ iext(uri_rdf_first,sK18,X3) ) ).

cnf(u2265,axiom,
    ~ iext(sK1(uri_owl_OntologyProperty,uri_ex_hasFather),X0,X1) ).

cnf(u364,axiom,
    ( ~ iext(uri_owl_someValuesFrom,X0,X2)
    | ~ iext(uri_owl_onProperty,X0,X1)
    | ~ icext(X2,X4)
    | ~ iext(X1,X3,X4)
    | icext(X0,X3) ) ).

cnf(u1797,axiom,
    ( ~ iext(sK9(uri_rdfs_domain,X0),X1,X2)
    | icext(sK10(uri_rdfs_domain,X0),X1)
    | iext(uri_rdfs_domain,uri_rdfs_domain,X0) ) ).

cnf(u1654,axiom,
    iext(uri_rdfs_range,X0,uri_rdfs_Literal) ).

cnf(u1995,axiom,
    ( icext(sK15(uri_rdfs_subClassOf,X0),sK4(sK14(uri_rdfs_subClassOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0)
    | iext(uri_owl_unionOf,sK14(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).

cnf(u2055,axiom,
    ( ~ iext(uri_owl_unionOf,X2,sK19)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK19,X0) ) ).

cnf(u2001,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK9(X1,sK10(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_rdfs_domain,X1,sK10(uri_owl_complementOf,X0)) ) ).

cnf(u237,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,X7)
    | ~ icext(X0,X7)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u469,axiom,
    iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,sK18) ).

cnf(u2015,axiom,
    ( icext(sK15(uri_rdfs_domain,X0),sK9(sK14(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0)
    | iext(uri_rdfs_domain,sK14(uri_rdfs_domain,X0),X1) ) ).

cnf(u354,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
    | iext(X1,X2,X3)
    | ~ iext(X0,X2,X3) ) ).

cnf(u2409,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,sK5(X0,X2))
    | icext(X0,sK5(X0,X2))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u1907,axiom,
    ( icext(sK15(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | icext(sK14(uri_owl_complementOf,X0),X1) ) ).

cnf(u1782,axiom,
    ( iext(X0,sK9(X0,X1),sK10(X0,X1))
    | iext(uri_rdfs_domain,X0,X1) ) ).

cnf(u212,axiom,
    ( ~ iext(uri_owl_complementOf,X0,X1)
    | icext(X1,X2)
    | icext(X0,X2) ) ).

cnf(u1913,axiom,
    ( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).

cnf(u983,axiom,
    ( ~ iext(sK4(uri_owl_OntologyProperty),X0,X1)
    | ix(X0) ) ).

cnf(u227,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,X5)
    | ~ icext(X0,X5)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u1799,axiom,
    ( ~ iext(uri_rdfs_subClassOf,sK10(uri_rdfs_subClassOf,X0),X1)
    | iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0)
    | iext(uri_rdfs_subClassOf,sK9(uri_rdfs_subClassOf,X0),X1) ) ).

cnf(u3032,axiom,
    iext(uri_rdfs_domain,X0,sK22) ).

cnf(u3154,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Class,sK21) ).

cnf(u254,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,X3)
    | ~ icext(X0,X3)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u3035,axiom,
    iext(uri_owl_intersectionOf,sK22,sK19) ).

cnf(u1814,axiom,
    ( iext(uri_rdfs_member,sK9(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK10(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
    | iext(uri_rdfs_domain,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u371,axiom,
    iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u2053,axiom,
    ( ~ iext(uri_owl_intersectionOf,X2,sK19)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK19,X0) ) ).

cnf(u2048,axiom,
    ( ~ iext(sK14(uri_rdfs_subPropertyOf,X0),sK14(X1,sK15(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK15(uri_rdfs_subPropertyOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,X1,sK15(uri_rdfs_subPropertyOf,X0)) ) ).

cnf(u1927,axiom,
    ( iext(uri_rdfs_member,sK14(uri_rdf__2,X0),sK15(uri_rdf__2,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ) ).

cnf(u266,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X6,X7)
    | icext(X4,X7)
    | icext(X2,X7)
    | ~ icext(X0,X7)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u4347,axiom,
    iext(uri_owl_intersectionOf,uri_owl_Thing,sK20) ).

cnf(u2054,axiom,
    ( ~ iext(uri_owl_intersectionOf,X2,sK21)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK21,X0) ) ).

cnf(u3471,axiom,
    iext(uri_rdfs_range,sK2(uri_owl_OntologyProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ).

cnf(u2024,axiom,
    ( icext(sK10(uri_owl_someValuesFrom,X0),sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
    | ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK9(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).

cnf(u4087,axiom,
    iext(uri_owl_unionOf,uri_ex_hasCousin,sK21) ).

cnf(u1804,axiom,
    ( iext(uri_rdfs_member,sK9(uri_rdf__2,X0),sK10(uri_rdf__2,X0))
    | iext(uri_rdfs_domain,uri_rdf__2,X0) ) ).

cnf(u4093,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasCousin,sK21) ).

cnf(u4148,axiom,
    iext(uri_rdfs_domain,X0,uri_rdfs_Datatype) ).

cnf(u1802,axiom,
    ( iext(sK10(uri_rdfs_subPropertyOf,X0),X1,X2)
    | iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
    | ~ iext(sK9(uri_rdfs_subPropertyOf,X0),X1,X2) ) ).

cnf(u2332,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK1(X0,X2))
    | ~ icext(X0,sK1(X0,X2))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u3749,axiom,
    ( ~ iext(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u4091,axiom,
    iext(uri_rdfs_range,X0,uri_ex_hasCousin) ).

cnf(u1926,axiom,
    ( iext(uri_rdfs_member,sK14(uri_rdf__1,X0),sK15(uri_rdf__1,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ) ).

cnf(u392,axiom,
    iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).

cnf(u1640,axiom,
    iext(uri_rdfs_domain,X0,uri_rdf_Property) ).

cnf(u1932,axiom,
    ( icext(uri_rdfs_Statement,sK14(uri_rdf_predicate,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ) ).

cnf(u3109,axiom,
    iext(uri_owl_unionOf,uri_ex_hasFather,sK19) ).

cnf(u1930,axiom,
    ( icext(uri_rdfs_Statement,sK14(uri_rdf_subject,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0) ) ).

cnf(u411,axiom,
    iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).

cnf(u3750,axiom,
    iext(uri_rdfs_domain,sK2(uri_owl_OntologyProperty,uri_ex_hasUncle,sK22),X0) ).

cnf(u3113,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK5(sK10(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK10(uri_owl_complementOf,X0),sK19) ) ).

cnf(u1909,axiom,
    ( icext(uri_rdf_List,sK14(uri_rdf_first,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0) ) ).

cnf(u1673,axiom,
    iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ).

cnf(u3110,axiom,
    iext(uri_owl_unionOf,sK22,sK19) ).

cnf(u4146,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Datatype,sK18) ).

cnf(u3103,axiom,
    ( ~ icext(X0,sK5(X0,uri_ex_hasFather))
    | iext(uri_owl_unionOf,X0,sK19) ) ).

cnf(u1848,axiom,
    ( icext(uri_rdf_List,sK12(uri_rdf_rest,X0))
    | iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).

cnf(u1568,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ) ).

cnf(u4401,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK20)
    | ~ iext(uri_rdf_first,sK20,X1)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ icext(X3,sK3(X4,X3,X1,X0))
    | ~ icext(X4,sK3(X4,X3,X1,X0))
    | iext(uri_owl_intersectionOf,X4,X2) ) ).

cnf(u3231,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK6(sK15(uri_owl_complementOf,X0),uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),sK18) ) ).

cnf(u2355,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | ~ icext(X0,sK1(X1,X0))
    | ~ icext(X1,sK1(X1,X0))
    | iext(uri_owl_intersectionOf,X1,sK21) ) ).

cnf(u3911,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK18)
    | icext(X0,X2)
    | ~ icext(X3,X2)
    | ~ icext(X4,X2)
    | ~ iext(uri_rdf_first,X1,X3)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,sK18,X4) ) ).

cnf(u2991,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,sK2(X0,X2,X4))
    | ~ icext(X2,sK2(X0,X2,X4))
    | ~ icext(X0,sK2(X0,X2,X4))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2615,axiom,
    ( ~ icext(X0,sK1(X0,uri_ex_hasFather))
    | ~ icext(uri_ex_hasFather,sK1(X0,uri_ex_hasFather))
    | iext(uri_owl_intersectionOf,X0,sK19) ) ).

cnf(u3285,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK1(sK10(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),sK19) ) ).

cnf(u1467,axiom,
    ( ~ iext(uri_rdf__2,X0,X1)
    | iext(uri_rdfs_member,X0,X1) ) ).

cnf(u1853,axiom,
    ( icext(uri_owl_Restriction,sK11(uri_owl_hasValue,X0))
    | iext(uri_rdfs_range,uri_owl_hasValue,X0) ) ).

cnf(u3128,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X6,sK3(X0,X2,X4,X6))
    | ~ icext(X4,sK3(X0,X2,X4,X6))
    | ~ icext(X2,sK3(X0,X2,X4,X6))
    | ~ icext(X0,sK3(X0,X2,X4,X6))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u349,axiom,
    ( ~ iext(uri_rdfs_subClassOf,X0,X1)
    | icext(X1,X2)
    | ~ icext(X0,X2) ) ).

cnf(u3252,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,sK18)
    | icext(X0,X1)
    | ~ icext(X2,X1)
    | ~ iext(uri_rdf_first,sK18,X2) ) ).

cnf(u1851,axiom,
    ( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
    | iext(uri_rdfs_range,uri_rdf_type,X0) ) ).

cnf(u2894,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X4,sK6(X0,X2,X4))
    | ~ icext(X0,sK6(X0,X2,X4))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u2900,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X3,sK6(X3,X2,X0))
    | iext(uri_owl_unionOf,X3,X1) ) ).

cnf(u1979,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK13(X1,sK15(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,X1,sK15(uri_owl_complementOf,X0)) ) ).

cnf(u3159,axiom,
    iext(uri_owl_unionOf,sK22,sK21) ).

cnf(u1857,axiom,
    ( icext(uri_owl_Restriction,sK11(uri_owl_someValuesFrom,X0))
    | iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).

cnf(u325,axiom,
    ( ~ iext(uri_owl_intersectionOf,X0,X1)
    | icext(uri_rdf_List,X1) ) ).

cnf(u455,axiom,
    iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave) ).

cnf(u3028,axiom,
    icext(sK22,X0) ).

cnf(u1638,axiom,
    iext(uri_rdfs_domain,X0,uri_owl_Thing) ).

cnf(u1736,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0)
    | iext(uri_rdfs_subClassOf,X1,X0) ) ).

cnf(u366,axiom,
    iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).

cnf(u3033,axiom,
    iext(uri_rdfs_range,X0,sK22) ).

cnf(u1893,axiom,
    ( ~ icext(sK11(uri_owl_complementOf,X0),sK4(sK12(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK12(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u367,axiom,
    iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).

cnf(u4291,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasUncle,uri_rdf_nil) ).

cnf(u1897,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK12(X1,sK12(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_rdfs_range,X1,sK12(uri_owl_complementOf,X0)) ) ).

cnf(u4222,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasFather,sK18) ).

cnf(u2782,axiom,
    ( iext(uri_rdfs_member,sK11(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0),sK12(sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0))
    | iext(uri_rdfs_range,sK1(uri_rdfs_ContainerMembershipProperty,sK22),X0) ) ).

cnf(u365,axiom,
    iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).

cnf(u1911,axiom,
    ( icext(uri_rdf_List,sK14(uri_rdf_rest,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).

cnf(u466,axiom,
    iext(uri_rdf_first,sK19,uri_ex_hasFather) ).

cnf(u2019,axiom,
    ( icext(sK15(uri_rdfs_range,X0),sK12(sK14(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0)
    | iext(uri_rdfs_range,sK14(uri_rdfs_range,X0),X1) ) ).

cnf(u238,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X2,X7)
    | ~ icext(X0,X7)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2417,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK5(X0,X2))
    | ~ icext(X0,sK5(X0,X2))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u4032,axiom,
    iext(uri_rdfs_range,X0,uri_owl_DatatypeProperty) ).

cnf(u464,axiom,
    iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,sK20) ).

cnf(u3034,axiom,
    iext(uri_rdfs_subClassOf,X0,sK22) ).

cnf(u1798,axiom,
    ( ~ iext(sK9(uri_rdfs_range,X0),X2,X1)
    | icext(sK10(uri_rdfs_range,X0),X1)
    | iext(uri_rdfs_domain,uri_rdfs_range,X0) ) ).

cnf(u236,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X6,X7)
    | ~ icext(X0,X7)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2021,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
    | ~ icext(X1,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
    | icext(sK9(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).

cnf(u1844,axiom,
    ( ~ icext(sK12(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | ~ icext(sK11(uri_owl_complementOf,X0),X1) ) ).

cnf(u2025,axiom,
    ( icext(sK12(uri_owl_someValuesFrom,X0),sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
    | ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK11(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).

cnf(u1910,axiom,
    ( icext(uri_rdf_List,sK15(uri_rdf_rest,X0))
    | iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).

cnf(u2288,axiom,
    iext(uri_rdfs_range,sK1(uri_owl_OntologyProperty,uri_ex_hasFather),X0) ).

cnf(u2008,axiom,
    ( icext(sK10(uri_rdfs_subClassOf,X0),sK4(sK9(uri_rdfs_subClassOf,X0)))
    | iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0)
    | iext(uri_owl_unionOf,sK9(uri_rdfs_subClassOf,X0),uri_rdf_nil) ) ).

cnf(u1513,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u1916,axiom,
    ( ~ iext(uri_owl_hasValue,sK14(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
    | iext(sK15(uri_owl_onProperty,X0),X2,X1)
    | ~ icext(sK14(uri_owl_onProperty,X0),X2) ) ).

cnf(u2061,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
    | ~ iext(sK15(uri_owl_onProperty,X0),X2,X3)
    | icext(X1,X3)
    | ~ icext(sK14(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).

cnf(u1914,axiom,
    ( icext(uri_owl_Restriction,sK14(uri_owl_allValuesFrom,X0))
    | iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ) ).

cnf(u267,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X6,X7)
    | icext(X0,X7)
    | ~ iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u382,axiom,
    iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).

cnf(u1792,axiom,
    ( icext(uri_owl_Restriction,sK9(uri_owl_hasValue,X0))
    | iext(uri_rdfs_domain,uri_owl_hasValue,X0) ) ).

cnf(u1297,axiom,
    ( ~ iext(uri_rdf_rest,X1,X0)
    | icext(uri_rdf_List,X0) ) ).

cnf(u4081,axiom,
    icext(uri_ex_hasCousin,X0) ).

cnf(u4095,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasCousin,uri_rdf_nil) ).

cnf(u2067,axiom,
    ( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
    | iext(X1,X2,sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
    | ~ icext(sK14(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).

cnf(u1822,axiom,
    iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Restriction) ).

cnf(u1920,axiom,
    ( ~ iext(sK14(uri_rdfs_domain,X0),X1,X2)
    | icext(sK15(uri_rdfs_domain,X0),X1)
    | iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0) ) ).

cnf(u1828,axiom,
    iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Restriction) ).

cnf(u1179,axiom,
    ~ icext(uri_rdf_XMLLiteral,X0) ).

cnf(u1785,axiom,
    ( icext(uri_rdf_List,sK10(uri_owl_intersectionOf,X0))
    | iext(uri_rdfs_domain,uri_owl_intersectionOf,X0) ) ).

cnf(u3221,axiom,
    ( ~ iext(uri_rdf_first,sK18,X0)
    | ~ icext(X1,sK6(X1,X0,uri_ex_hasFather))
    | iext(uri_owl_unionOf,X1,sK18) ) ).

cnf(u4356,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasFather,sK20) ).

cnf(u4250,axiom,
    ( ~ iext(uri_rdf_first,sK20,X0)
    | ~ icext(X0,sK2(X1,X0,sK22))
    | ~ icext(X1,sK2(X1,X0,sK22))
    | iext(uri_owl_intersectionOf,X1,sK20) ) ).

cnf(u1671,axiom,
    ( iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),uri_rdfs_member)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u393,axiom,
    iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1214,axiom,
    ( ~ iext(uri_rdf_subject,X0,X1)
    | icext(uri_rdfs_Statement,X0) ) ).

cnf(u1569,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
    | iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ) ).

cnf(u3222,axiom,
    ( ~ icext(X0,sK6(X0,uri_ex_hasCousin,uri_ex_hasFather))
    | iext(uri_owl_unionOf,X0,sK18) ) ).

cnf(u1693,axiom,
    ( ~ iext(sK13(uri_owl_OntologyProperty,X0),X1,X2)
    | iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ) ).

cnf(u4248,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK2(X3,X2,X0))
    | ~ icext(X3,sK2(X3,X2,X0))
    | iext(uri_owl_intersectionOf,X3,X1) ) ).

cnf(u2289,axiom,
    iext(uri_rdfs_subPropertyOf,sK1(uri_owl_OntologyProperty,uri_ex_hasFather),X0) ).

cnf(u3470,axiom,
    iext(uri_rdfs_domain,sK2(uri_owl_OntologyProperty,uri_ex_hasCousin,uri_ex_hasFather),X0) ).

cnf(u1674,axiom,
    iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),X0) ).

cnf(u4023,axiom,
    iodp(X0) ).

cnf(u1697,axiom,
    ( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X1)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
    | iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).

cnf(u1588,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Literal,uri_rdf_nil) ).

cnf(u4134,axiom,
    ( ~ iext(uri_rdf_rest,X2,sK18)
    | ~ iext(uri_rdf_first,sK18,X1)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X2,X3)
    | ~ icext(X4,sK7(X4,X3,X1,X0))
    | iext(uri_owl_unionOf,X4,X2) ) ).

cnf(u223,axiom,
    ( ~ iext(uri_rdf_rest,X1,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,X3)
    | icext(X0,X3)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u3112,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK5(sK15(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_unionOf,sK15(uri_owl_complementOf,X0),sK19) ) ).

cnf(u311,axiom,
    ( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
    | ix(X0) ) ).

cnf(u2105,axiom,
    ( ~ iext(uri_rdf_first,sK19,X0)
    | icext(X0,sK1(X1,X0))
    | icext(X1,sK1(X1,X0))
    | iext(uri_owl_intersectionOf,X1,sK19) ) ).

cnf(u1471,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0)
    | iext(uri_rdfs_subClassOf,X1,X0)
    | ~ ic(X1) ) ).

cnf(u439,axiom,
    ( ~ iext(uri_rdfs_subClassOf,X0,X1)
    | ~ iext(uri_rdfs_subClassOf,X1,X2)
    | iext(uri_rdfs_subClassOf,X0,X2) ) ).

cnf(u2106,axiom,
    ( ~ iext(uri_rdf_first,sK21,X0)
    | icext(X0,sK1(X1,X0))
    | icext(X1,sK1(X1,X0))
    | iext(uri_owl_intersectionOf,X1,sK21) ) ).

cnf(u4267,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Datatype,sK20) ).

cnf(u3260,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK18)
    | ~ icext(X0,X2)
    | icext(X3,X2)
    | ~ iext(uri_rdf_first,X1,X4)
    | ~ iext(uri_owl_intersectionOf,X0,X1)
    | ~ iext(uri_rdf_first,sK18,X3) ) ).

cnf(u2903,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X2,sK6(X0,X2,X4))
    | ~ icext(X0,sK6(X0,X2,X4))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u3284,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK1(sK15(uri_owl_complementOf,X0),uri_ex_hasFather))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),sK19) ) ).

cnf(u332,axiom,
    ( ~ iext(uri_owl_someValuesFrom,X0,X1)
    | icext(uri_owl_Restriction,X0) ) ).

cnf(u1707,axiom,
    iext(uri_rdfs_subClassOf,X0,X0) ).

cnf(u2875,axiom,
    iext(uri_owl_intersectionOf,uri_ex_hasFather,uri_rdf_nil) ).

cnf(u3271,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK20)
    | icext(X0,X2)
    | ~ icext(X3,X2)
    | ~ iext(uri_rdf_first,X1,X4)
    | ~ iext(uri_owl_unionOf,X0,X1)
    | ~ iext(uri_rdf_first,sK20,X3) ) ).

cnf(u1202,axiom,
    ( ~ iext(uri_rdf_first,X0,X1)
    | icext(uri_rdf_List,X0) ) ).

cnf(u1877,axiom,
    iext(uri_rdfs_range,sK4(uri_owl_OntologyProperty),X0) ).

cnf(u705,axiom,
    ( ~ icext(uri_owl_OntologyProperty,X0)
    | ioxp(X0) ) ).

cnf(u460,axiom,
    iext(uri_rdf_rest,sK21,uri_rdf_nil) ).

cnf(u1875,axiom,
    ( iext(uri_rdfs_range,sK13(uri_owl_OntologyProperty,X0),X1)
    | iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ) ).

cnf(u1221,axiom,
    icext(uri_rdf_List,sK18) ).

cnf(u3067,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK21)
    | ~ iext(uri_rdf_first,sK21,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | icext(X2,sK3(X5,X4,X2,X0))
    | icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u1881,axiom,
    iext(uri_rdfs_range,uri_owl_intersectionOf,uri_rdf_List) ).

cnf(u1476,axiom,
    ( ~ iext(uri_rdfs_subClassOf,uri_rdf_Property,X0)
    | iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).

cnf(u2005,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK0(sK10(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK10(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u2003,axiom,
    ( icext(sK9(uri_owl_complementOf,X0),sK13(X1,sK10(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,X1,sK10(uri_owl_complementOf,X0)) ) ).

cnf(u722,axiom,
    icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).

cnf(u2009,axiom,
    ( icext(sK12(uri_rdfs_domain,X0),sK9(sK11(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_range,uri_rdfs_domain,X0)
    | iext(uri_rdfs_domain,sK11(uri_rdfs_domain,X0),X1) ) ).

cnf(u1808,axiom,
    ( iext(uri_rdfs_seeAlso,sK9(uri_rdfs_isDefinedBy,X0),sK10(uri_rdfs_isDefinedBy,X0))
    | iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ) ).

cnf(u339,axiom,
    ( ~ iext(uri_rdfs_domain,X0,X1)
    | icext(X1,X2)
    | ~ iext(X0,X2,X3) ) ).

cnf(u2023,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
    | ~ icext(X1,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
    | icext(sK14(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).

cnf(u362,axiom,
    ( ~ iext(uri_owl_someValuesFrom,X0,X2)
    | ~ iext(uri_owl_onProperty,X0,X1)
    | icext(X2,sK17(X1,X2,X3))
    | ~ icext(X0,X3) ) ).

cnf(u3145,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X6,sK7(X0,X2,X4,X6))
    | icext(X4,sK7(X0,X2,X4,X6))
    | icext(X2,sK7(X0,X2,X4,X6))
    | icext(X0,sK7(X0,X2,X4,X6))
    | iext(uri_owl_unionOf,X0,X1) ) ).

cnf(u3105,axiom,
    iext(uri_owl_unionOf,uri_rdfs_Class,sK19) ).

cnf(u467,axiom,
    iext(uri_rdf_rest,sK18,sK19) ).

cnf(u360,axiom,
    ( ~ iext(uri_owl_onProperty,X0,X1)
    | ~ iext(uri_owl_hasValue,X0,X2)
    | ~ iext(X1,X3,X2)
    | icext(X0,X3) ) ).

cnf(u1992,axiom,
    ( icext(sK14(uri_owl_complementOf,X0),sK0(sK15(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK15(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u1900,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK0(sK12(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),uri_rdf_nil) ) ).

cnf(u1898,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK13(X1,sK12(uri_owl_complementOf,X0)))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_rdfs_subClassOf,X1,sK12(uri_owl_complementOf,X0)) ) ).

cnf(u2022,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
    | ~ icext(X1,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
    | icext(sK11(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).

cnf(u4223,axiom,
    iext(uri_owl_intersectionOf,sK22,sK18) ).

cnf(u2778,axiom,
    ( ~ iext(uri_rdf_rest,X3,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | icext(X4,sK2(X0,X2,X4))
    | icext(X0,sK2(X0,X2,X4))
    | iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u1641,axiom,
    iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).

cnf(u2028,axiom,
    ( icext(sK10(uri_rdfs_domain,X0),sK11(sK9(uri_rdfs_domain,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_domain,X0)
    | iext(uri_rdfs_range,sK9(uri_rdfs_domain,X0),X1) ) ).

cnf(u4215,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Class,sK18) ).

cnf(u4352,axiom,
    iext(uri_owl_intersectionOf,uri_rdfs_Resource,sK20) ).

cnf(u239,axiom,
    ( ~ iext(uri_rdf_rest,X5,uri_rdf_nil)
    | ~ iext(uri_rdf_first,X5,X6)
    | ~ iext(uri_rdf_rest,X3,X5)
    | ~ iext(uri_rdf_first,X3,X4)
    | ~ iext(uri_rdf_rest,X1,X3)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ icext(X6,X7)
    | ~ icext(X4,X7)
    | ~ icext(X2,X7)
    | icext(X0,X7)
    | ~ iext(uri_owl_intersectionOf,X0,X1) ) ).

cnf(u2026,axiom,
    ( icext(sK15(uri_owl_someValuesFrom,X0),sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
    | ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
    | ~ icext(sK14(uri_owl_someValuesFrom,X0),X2)
    | iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).

cnf(u2051,axiom,
    ( ~ iext(uri_owl_intersectionOf,X2,sK19)
    | ~ icext(X0,X1)
    | icext(X2,X1)
    | ~ iext(uri_rdf_first,sK19,X0) ) ).

cnf(u1806,axiom,
    ( icext(uri_rdfs_Statement,sK9(uri_rdf_object,X0))
    | iext(uri_rdfs_domain,uri_rdf_object,X0) ) ).

cnf(u3861,axiom,
    ( iext(uri_rdfs_member,sK11(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0),sK12(sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0))
    | iext(uri_rdfs_range,sK2(uri_rdfs_ContainerMembershipProperty,uri_ex_hasUncle,sK22),X0) ) ).

cnf(u2032,axiom,
    ( icext(sK10(uri_rdfs_range,X0),sK15(sK9(uri_rdfs_range,X0),X1))
    | iext(uri_rdfs_domain,uri_rdfs_range,X0)
    | iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_range,X0),X1) ) ).

cnf(u4351,axiom,
    iext(uri_owl_intersectionOf,uri_rdf_Property,sK20) ).

cnf(u250,axiom,
    ( icext(X0,sK4(X0))
    | ~ ic(X0)
    | iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).

cnf(u3081,axiom,
    ( ~ iext(uri_rdf_rest,X1,sK19)
    | ~ iext(uri_rdf_first,sK19,X0)
    | ~ iext(uri_rdf_first,X1,X2)
    | ~ iext(uri_rdf_rest,X3,X1)
    | ~ iext(uri_rdf_first,X3,X4)
    | icext(X4,sK3(X5,X4,X2,X0))
    | icext(X5,sK3(X5,X4,X2,X0))
    | iext(uri_owl_intersectionOf,X5,X3) ) ).

cnf(u1812,axiom,
    ( iext(uri_rdfs_member,sK9(sK4(uri_rdfs_ContainerMembershipProperty),X0),sK10(sK4(uri_rdfs_ContainerMembershipProperty),X0))
    | iext(uri_rdfs_domain,sK4(uri_rdfs_ContainerMembershipProperty),X0) ) ).

cnf(u2078,axiom,
    ( ~ iext(sK9(uri_rdfs_subPropertyOf,X0),sK14(X1,sK10(uri_rdfs_subPropertyOf,X0)),sK15(X1,sK10(uri_rdfs_subPropertyOf,X0)))
    | iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0)
    | iext(uri_rdfs_subPropertyOf,X1,sK10(uri_rdfs_subPropertyOf,X0)) ) ).

cnf(u4358,axiom,
    ( icext(sK11(uri_owl_complementOf,X0),sK2(sK12(uri_owl_complementOf,X0),uri_ex_hasUncle,sK22))
    | iext(uri_rdfs_range,uri_owl_complementOf,X0)
    | iext(uri_owl_intersectionOf,sK12(uri_owl_complementOf,X0),sK20) ) ).

cnf(u1855,axiom,
    ( ~ iext(uri_owl_hasValue,sK11(uri_owl_onProperty,X0),X1)
    | iext(uri_rdfs_range,uri_owl_onProperty,X0)
    | ~ iext(sK12(uri_owl_onProperty,X0),X2,X1)
    | icext(sK11(uri_owl_onProperty,X0),X2) ) ).

cnf(u3865,axiom,
    iext(uri_owl_unionOf,uri_owl_Thing,sK20) ).

cnf(u1783,axiom,
    ( ~ icext(sK10(uri_owl_complementOf,X0),X1)
    | iext(uri_rdfs_domain,uri_owl_complementOf,X0)
    | ~ icext(sK9(uri_owl_complementOf,X0),X1) ) ).

cnf(u2060,axiom,
    ( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
    | ~ iext(sK12(uri_owl_onProperty,X0),X2,X3)
    | icext(X1,X3)
    | ~ icext(sK11(uri_owl_onProperty,X0),X2)
    | iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).

cnf(u278,axiom,
    ~ icext(uri_owl_Nothing,X0) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWB025+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.35  % Computer : n001.cluster.edu
% 0.10/0.35  % Model    : x86_64 x86_64
% 0.10/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35  % Memory   : 8046.5625MB
% 0.10/0.35  % OS       : Linux 6.8.0-71-generic
% 0.10/0.35  % CPULimit : 300
% 0.10/0.35  % WCLimit  : 300
% 0.10/0.35  % DateTime : Mon Sep 28 07:11:33 UTC 2026
% 0.10/0.36  % CPUTime  : 
% 0.10/0.36  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39  Running first-order model finding
% 0.10/0.39  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.72/0.63  % (177131)Will run a generic schedule for satisfiability detection.
% 0.72/0.63  % (177140)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3360948733:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.72/0.63  % (177137)% WARNING: option uhcvi not known.
% 0.72/0.63  % (177139)dis+10_1_sil=32000:sp=arity:random_seed=4157341654:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.72/0.63  % (177136)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=964226519_2999 on theBenchmark for (2999ds/0Mi)
% 0.72/0.63  % (177137)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1735863245:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.72/0.63  % (177138)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1043925151:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.72/0.63  % (177141)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2848623697:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.72/0.63  % (177142)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2887234809:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.72/0.63  % TRYING [1]
% 0.72/0.63  % TRYING [2]
% 0.72/0.63  % (177140)Instruction limit reached! 
% 0.72/0.63  % (177140)------------------------------
% 0.72/0.63  % (177140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.63  % (177140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.63  % (177140)CaDiCaL version: 2.1.3
% 0.72/0.63  % (177140)Termination reason: Instruction limit
% 0.72/0.63  % (177140)Termination phase: Saturation
% 0.72/0.63  % (177140)Time elapsed: 0.027 s
% 0.72/0.63  % (177140)Peak memory usage: 11 MB
% 0.72/0.63  % (177140)Instructions burned: 119 (million)
% 0.72/0.63  % TRYING [3]
% 0.72/0.63  % (177150)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1170087030:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.72/0.63  % TRYING [1]
% 0.72/0.63  % TRYING [2]
% 0.72/0.63  % TRYING [3]
% 0.72/0.63  % TRYING [4]
% 0.72/0.63  % TRYING [4]
% 0.72/0.63  % (177139)Instruction limit reached! 
% 0.72/0.63  % (177139)------------------------------
% 0.72/0.63  % (177139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.63  % (177139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.63  % (177139)CaDiCaL version: 2.1.3
% 0.72/0.63  % (177139)Termination reason: Instruction limit
% 0.72/0.63  % (177139)Termination phase: Saturation
% 0.72/0.63  % (177139)Time elapsed: 0.061 s
% 0.72/0.63  % (177139)Peak memory usage: 13 MB
% 0.72/0.63  % (177139)Instructions burned: 104 (million)
% 0.72/0.63  % (177141)Instruction limit reached! 
% 0.72/0.63  % (177141)------------------------------
% 0.72/0.63  % (177141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.63  % (177141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.63  % (177141)CaDiCaL version: 2.1.3
% 0.72/0.63  % (177141)Termination reason: Instruction limit
% 0.72/0.63  % (177141)Termination phase: Saturation
% 0.72/0.63  % (177141)Time elapsed: 0.068 s
% 0.72/0.63  % (177141)Peak memory usage: 13 MB
% 0.72/0.63  % (177141)Instructions burned: 132 (million)
% 0.72/0.63  % (177152)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3659495663:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.72/0.63  % (177153)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3298293175:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.72/0.63  % (177142)Instruction limit reached! 
% 0.72/0.63  % (177142)------------------------------
% 0.72/0.63  % (177142)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.63  % (177142)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.63  % (177142)CaDiCaL version: 2.1.3
% 0.72/0.63  % (177142)Termination reason: Instruction limit
% 0.72/0.63  % (177142)Termination phase: Saturation
% 0.72/0.63  % (177142)Time elapsed: 0.095 s
% 0.72/0.63  % (177142)Peak memory usage: 13 MB
% 0.72/0.63  % (177142)Instructions burned: 160 (million)
% 0.72/0.63  % (177156)ott-21_1_sil=16000:fs=off:random_seed=3710519370:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.72/0.63  % (177152)Instruction limit reached! 
% 0.72/0.63  % (177152)------------------------------
% 0.72/0.63  % (177152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.63  % (177152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.63  % (177152)CaDiCaL version: 2.1.3
% 0.72/0.63  % (177152)Termination reason: Instruction limit
% 0.72/0.63  % (177152)Termination phase: Saturation
% 0.72/0.63  % (177152)Time elapsed: 0.069 s
% 0.72/0.63  % (177152)Peak memory usage: 13 MB
% 0.72/0.63  % (177152)Instructions burned: 131 (million)
% 0.72/0.63  % (177158)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3029086936:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 0.72/0.63  % (177153) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-177131-177153"...
% 0.72/0.63  % (177153)...printing done.
% 0.72/0.63  % SZS status CounterSatisfiable for theBenchmark
% 0.72/0.63  % SZS output start Saturation.
% See solution above
% 0.72/0.64  % SZS output start Definitions and Model Updates.
% 0.72/0.64  for all groundings,
% 0.72/0.64      whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 0.72/0.64  for all groundings,
% 0.72/0.64      whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 0.72/0.64  for all groundings,
% 0.72/0.64      whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 0.72/0.64  for all groundings,
% 0.72/0.64      whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 0.72/0.64  % SZS output end Definitions and Model Updates.
% 0.72/0.64  % (177153)------------------------------
% 0.72/0.64  % (177153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.72/0.64  % (177153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.72/0.64  % (177153)CaDiCaL version: 2.1.3
% 0.72/0.64  % (177153)Termination reason: Satisfiable
% 0.72/0.64  % (177153)Time elapsed: 0.108 s
% 0.72/0.64  % (177153)Peak memory usage: 14 MB
% 0.72/0.64  % (177153)Instructions burned: 171 (million)
% 0.72/0.64  % (177131)Success in time 0.235 s
% 0.72/0.64  % Vampire exiting
%------------------------------------------------------------------------------