%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWB032+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 : n013.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:50 PM UTC 2026
% Result : CounterSatisfiable 0.92s 0.62s
% Output : Saturation 0.92s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u461,negated_conjecture,
~ iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal) ).
cnf(u468,axiom,
ic(uri_rdfs_Resource) ).
cnf(u505,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_rdfs_Resource) ).
cnf(u714,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,uri_owl_Thing) ).
cnf(u976,axiom,
( ioap(sK13(uri_owl_AnnotationProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0)
| ~ ic(X0) ) ).
cnf(u985,axiom,
( iodp(sK13(uri_owl_DatatypeProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0)
| ~ ic(X0) ) ).
cnf(u994,axiom,
( ioxp(sK13(uri_owl_OntologyProperty,X0))
| iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0)
| ~ ic(X0) ) ).
cnf(u1008,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0)
| ~ ic(X0) ) ).
cnf(u1115,axiom,
iext(uri_owl_unionOf,uri_rdfs_Statement,uri_rdf_nil) ).
cnf(u1128,axiom,
icext(uri_rdf_XMLLiteral,sK4(uri_rdf_XMLLiteral)) ).
cnf(u1133,axiom,
iext(uri_owl_unionOf,uri_rdfs_Seq,uri_rdf_nil) ).
cnf(u1141,axiom,
~ iext(uri_owl_unionOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_nil) ).
cnf(u1146,axiom,
icext(uri_rdfs_ContainerMembershipProperty,sK4(uri_rdfs_ContainerMembershipProperty)) ).
cnf(u1151,axiom,
iext(uri_owl_unionOf,uri_rdf_Bag,uri_rdf_nil) ).
cnf(u1164,axiom,
icext(uri_rdfs_Container,sK4(uri_rdfs_Container)) ).
cnf(u1169,axiom,
iext(uri_owl_unionOf,uri_rdf_Alt,uri_rdf_nil) ).
cnf(u1182,axiom,
icext(uri_rdf_List,sK4(uri_rdf_List)) ).
cnf(u1191,axiom,
icext(uri_rdfs_Literal,sK4(uri_rdfs_Literal)) ).
cnf(u1200,axiom,
icext(uri_rdf_Property,sK4(uri_rdf_Property)) ).
cnf(u1209,axiom,
icext(uri_rdfs_Datatype,sK4(uri_rdfs_Datatype)) ).
cnf(u1218,axiom,
icext(uri_rdfs_Class,sK4(uri_rdfs_Class)) ).
cnf(u1332,axiom,
icext(uri_rdfs_Class,uri_owl_Nothing) ).
cnf(u1402,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Datatype),uri_rdf_nil) ).
cnf(u1413,axiom,
iext(uri_owl_unionOf,sK4(uri_rdfs_Class),uri_rdf_nil) ).
cnf(u1637,axiom,
icext(uri_rdfs_Class,uri_rdfs_Literal) ).
cnf(u1642,axiom,
icext(uri_rdfs_Class,uri_rdfs_Class) ).
cnf(u1844,axiom,
( ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0) ) ).
cnf(u2421,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_member) ).
cnf(u2543,axiom,
iext(uri_owl_intersectionOf,uri_rdf_Property,uri_rdf_nil) ).
cnf(u2552,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Class,uri_rdf_nil) ).
cnf(u2719,axiom,
ix(sK4(uri_owl_Ontology)) ).
cnf(u2732,axiom,
iext(uri_owl_unionOf,uri_owl_OntologyProperty,uri_rdf_nil) ).
cnf(u2741,axiom,
iext(uri_owl_unionOf,uri_owl_DatatypeProperty,uri_rdf_nil) ).
cnf(u2750,axiom,
iext(uri_owl_unionOf,uri_owl_AnnotationProperty,uri_rdf_nil) ).
cnf(u3873,axiom,
icext(sK14(uri_owl_complementOf,uri_rdf_type),sK14(uri_owl_complementOf,uri_rdf_type)) ).
cnf(u3879,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(u1021,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).
cnf(u2831,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Class),X0) ).
cnf(u3082,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing) ) ).
cnf(u1553,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u3885,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(u3993,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK12(uri_rdfs_subClassOf,X1)) ) ).
cnf(u3675,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(u406,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).
cnf(u4007,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(u3353,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u678,axiom,
icext(uri_owl_Thing,X0) ).
cnf(u2589,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Resource) ).
cnf(u2587,axiom,
iext(uri_rdfs_domain,X0,uri_rdfs_Class) ).
cnf(u4141,axiom,
( iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),uri_rdfs_member)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).
cnf(u2079,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u293,axiom,
( ~ iodp(X0)
| ~ iext(X0,X1,X2)
| lv(X2) ) ).
cnf(u316,axiom,
( ~ iext(uri_owl_allValuesFrom,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u1715,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u3996,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(u3501,axiom,
( icext(uri_rdf_List,sK12(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_range,uri_owl_intersectionOf,X0) ) ).
cnf(u3994,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,sK12(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_subPropertyOf,sK11(uri_rdfs_subPropertyOf,X0),uri_rdfs_member)
| iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u3625,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(u421,axiom,
( ~ lv(X0)
| icext(uri_rdfs_Literal,X0) ) ).
cnf(u3505,axiom,
( icext(uri_rdf_List,sK12(uri_owl_unionOf,X0))
| iext(uri_rdfs_range,uri_owl_unionOf,X0) ) ).
cnf(u1606,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u3753,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ) ).
cnf(u3507,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_range,uri_owl_allValuesFrom,X0) ) ).
cnf(u2489,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u3924,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK13(uri_rdfs_Datatype,X0))
| lv(sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| iext(uri_rdfs_subClassOf,X1,X2) ) ).
cnf(u956,axiom,
( ~ icext(uri_rdf_XMLLiteral,X0)
| lv(X0) ) ).
cnf(u1094,axiom,
( ~ iext(uri_owl_intersectionOf,X0,uri_rdf_nil)
| icext(X0,X1) ) ).
cnf(u333,axiom,
( ~ iext(uri_owl_unionOf,X0,X1)
| icext(uri_rdf_List,X1) ) ).
cnf(u3922,axiom,
( iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| lv(sK4(sK13(uri_rdfs_Datatype,X0))) ) ).
cnf(u1987,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ) ).
cnf(u3527,axiom,
( iext(uri_rdfs_member,sK11(uri_rdf__3,X0),sK12(uri_rdf__3,X0))
| iext(uri_rdfs_range,uri_rdf__3,X0) ) ).
cnf(u1949,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u3539,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(u1222,axiom,
icext(uri_rdfs_Literal,sK4(uri_rdf_XMLLiteral)) ).
cnf(u346,axiom,
( icext(X0,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3531,axiom,
( iext(uri_rdfs_member,sK11(uri_rdfs_isDefinedBy,X0),sK12(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u3678,axiom,
( iext(uri_rdfs_member,sK9(uri_rdf__3,X0),sK10(uri_rdf__3,X0))
| iext(uri_rdfs_domain,uri_rdf__3,X0) ) ).
cnf(u3917,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| lv(sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u3791,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3684,axiom,
( icext(uri_rdfs_Literal,sK10(uri_rdfs_label,X0))
| iext(uri_rdfs_domain,uri_rdfs_label,X0) ) ).
cnf(u1220,axiom,
iext(uri_owl_unionOf,uri_owl_Nothing,uri_rdf_nil) ).
cnf(u451,axiom,
ir(X0) ).
cnf(u3534,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,X0) ).
cnf(u3682,axiom,
( iext(uri_rdfs_member,sK9(uri_rdfs_isDefinedBy,X0),sK10(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u2634,axiom,
( iext(X0,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u3430,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(u2930,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(u2775,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_OntologyProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u2657,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u363,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| ~ icext(X2,X4)
| ~ iext(X1,X3,X4)
| icext(X0,X3) ) ).
cnf(u2535,axiom,
iext(uri_owl_intersectionOf,uri_owl_Thing,uri_rdf_nil) ).
cnf(u3520,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(u3708,axiom,
( lv(sK10(uri_rdfs_label,X0))
| iext(uri_rdfs_domain,uri_rdfs_label,X0) ) ).
cnf(u1379,axiom,
( ~ iext(uri_rdfs_comment,X1,X0)
| icext(uri_rdfs_Literal,X0) ) ).
cnf(u3558,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(u3189,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u1015,axiom,
icext(uri_rdf_List,uri_rdf_nil) ).
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(u361,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| icext(X2,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u3845,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(u256,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(u3562,axiom,
( icext(uri_rdf_List,sK14(uri_rdf_first,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0) ) ).
cnf(u515,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u2559,axiom,
ic(X0) ).
cnf(u3572,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(u3863,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(u1291,axiom,
~ iext(uri_rdf_predicate,X0,X1) ).
cnf(u2713,axiom,
( iext(uri_owl_unionOf,sK13(uri_rdfs_Datatype,X0),uri_rdf_nil)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| lv(sK4(sK13(uri_rdfs_Datatype,X0))) ) ).
cnf(u3576,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK15(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u3661,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| ~ iext(sK10(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u2714,axiom,
( icext(uri_rdfs_Literal,sK4(sK13(uri_rdfs_Datatype,X0)))
| iext(uri_owl_unionOf,sK13(uri_rdfs_Datatype,X0),uri_rdf_nil)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u3659,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_hasValue,X0))
| iext(uri_rdfs_domain,uri_owl_hasValue,X0) ) ).
cnf(u3846,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(u2573,axiom,
ip(X0) ).
cnf(u1571,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ) ).
cnf(u1025,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).
cnf(u3852,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(u2435,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u3850,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(u277,axiom,
~ icext(uri_owl_Nothing,X0) ).
cnf(u3856,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(u407,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).
cnf(u300,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_OntologyProperty)
| ioxp(X0) ) ).
cnf(u2565,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0) ).
cnf(u4142,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(u405,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).
cnf(u3902,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(u3493,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(u3627,axiom,
( ~ icext(sK15(X0,uri_rdf_type),sK14(X0,uri_rdf_type))
| iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type) ) ).
cnf(u3740,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).
cnf(u769,axiom,
idc(uri_rdf_XMLLiteral) ).
cnf(u3511,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
| icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u3908,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(u445,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| iext(uri_rdfs_subPropertyOf,X0,X2) ) ).
cnf(u3515,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK12(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK11(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u3912,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(u959,axiom,
( ~ icext(uri_rdfs_Datatype,X0)
| idc(X0) ) ).
cnf(u2636,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3899,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(u3518,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0) ) ).
cnf(u1023,axiom,
icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).
cnf(u2112,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt) ) ).
cnf(u1241,axiom,
~ icext(uri_rdf_Bag,X0) ).
cnf(u2758,axiom,
iext(uri_rdfs_subClassOf,uri_owl_OntologyProperty,X0) ).
cnf(u1229,axiom,
~ icext(uri_rdfs_Seq,X0) ).
cnf(u3668,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)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u3685,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,X0) ).
cnf(u328,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u3535,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(u3666,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| ~ icext(sK10(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK9(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u3683,axiom,
( iext(uri_rdfs_seeAlso,sK9(uri_rdfs_isDefinedBy,X0),sK10(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u3672,axiom,
( ~ icext(sK9(uri_rdfs_subClassOf,X0),X1)
| icext(sK10(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0) ) ).
cnf(u2759,axiom,
~ icext(uri_owl_DatatypeProperty,X0) ).
cnf(u3522,axiom,
( iext(uri_rdfs_subClassOf,X1,sK12(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK11(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u347,axiom,
( ~ icext(X1,sK13(X0,X1))
| ~ ic(X1)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3686,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(u2655,axiom,
( ~ iext(X1,sK14(X0,X1),sK15(X0,X1))
| iext(uri_rdfs_subPropertyOf,X0,X1) ) ).
cnf(u1996,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u3542,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(u2269,axiom,
( ~ iext(uri_rdf__2,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u999,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X0)
| lv(X1) ) ).
cnf(u2752,axiom,
iext(uri_rdf_type,sK4(uri_owl_Ontology),uri_owl_Ontology) ).
cnf(u2147,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ) ).
cnf(u368,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).
cnf(u3546,axiom,
iext(uri_rdfs_range,uri_owl_intersectionOf,uri_rdf_List) ).
cnf(u2129,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ) ).
cnf(u3301,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_XMLLiteral) ) ).
cnf(u968,axiom,
( idc(sK13(uri_rdfs_Datatype,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u3915,axiom,
( iext(uri_rdfs_member,sK14(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK15(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_subPropertyOf,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u2156,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u4085,axiom,
( iext(uri_rdfs_subClassOf,sK15(uri_owl_complementOf,X0),sK15(uri_owl_complementOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0) ) ).
cnf(u2036,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u3560,axiom,
( icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| icext(sK14(uri_owl_complementOf,X0),X1) ) ).
cnf(u247,axiom,
( ~ iext(uri_owl_unionOf,X0,uri_rdf_nil)
| ~ icext(X0,X1) ) ).
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(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u372,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).
cnf(u1777,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u3580,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(u3573,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(u2554,axiom,
icext(uri_rdfs_Class,X0) ).
cnf(u2268,axiom,
( ~ iext(uri_rdf__1,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u3577,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)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK14(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u2813,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_AnnotationProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u391,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).
cnf(u1580,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
cnf(u3593,axiom,
( icext(uri_rdfs_Literal,sK15(uri_rdfs_label,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ) ).
cnf(u285,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Class)
| ~ ic(X0) ) ).
cnf(u1430,axiom,
~ icext(sK4(uri_rdfs_Class),X0) ).
cnf(u389,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).
cnf(u3607,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(u3886,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(u790,axiom,
iext(uri_rdf_type,X0,uri_rdfs_Resource) ).
cnf(u3613,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(u3892,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(u3594,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,X0) ).
cnf(u2103,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u3890,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(u3617,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(u4014,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X1) ) ).
cnf(u3896,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(u3741,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ) ).
cnf(u3588,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_object,X0) ).
cnf(u2607,axiom,
( iext(X0,sK11(X0,X1),sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u314,axiom,
( iext(uri_rdf_type,X0,uri_rdfs_Literal)
| ~ lv(X0) ) ).
cnf(u3499,axiom,
( ~ icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| ~ icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u3646,axiom,
( lv(sK15(uri_rdfs_label,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_label,X0) ) ).
cnf(u3883,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(u3502,axiom,
( icext(uri_rdf_List,sK11(uri_rdf_first,X0))
| iext(uri_rdfs_range,uri_rdf_first,X0) ) ).
cnf(u3519,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(u1031,axiom,
( lv(sK13(sK13(uri_rdfs_Datatype,X0),X1))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1) ) ).
cnf(u3889,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(u2484,axiom,
( ~ icext(X0,sK0(X0))
| ~ ic(X0)
| iext(uri_owl_intersectionOf,X0,uri_rdf_nil) ) ).
cnf(u3903,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(u3506,axiom,
( icext(sK12(uri_rdf_type,X0),sK11(uri_rdf_type,X0))
| iext(uri_rdfs_range,uri_rdf_type,X0) ) ).
cnf(u3652,axiom,
( icext(uri_rdf_List,sK10(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_domain,uri_owl_intersectionOf,X0) ) ).
cnf(u3669,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0) ) ).
cnf(u4011,axiom,
iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),uri_rdfs_member) ).
cnf(u2375,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,X1,X0)
| ~ icext(uri_rdfs_ContainerMembershipProperty,X1) ) ).
cnf(u3650,axiom,
( ~ icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| ~ icext(sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u3667,axiom,
( ~ iext(uri_owl_onProperty,sK9(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK10(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK9(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u3656,axiom,
( icext(uri_rdf_List,sK10(uri_owl_unionOf,X0))
| iext(uri_rdfs_domain,uri_owl_unionOf,X0) ) ).
cnf(u2898,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Resource) ).
cnf(u1978,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
cnf(u964,axiom,
( ~ icext(uri_owl_Ontology,X0)
| ix(X0) ) ).
cnf(u331,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u3670,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(u2373,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u3676,axiom,
( iext(uri_rdfs_member,sK9(uri_rdf__1,X0),sK10(uri_rdf__1,X0))
| iext(uri_rdfs_domain,uri_rdf__1,X0) ) ).
cnf(u590,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u2753,axiom,
~ icext(uri_owl_OntologyProperty,X0) ).
cnf(u3530,axiom,
( icext(uri_rdfs_Literal,sK12(uri_rdfs_comment,X0))
| iext(uri_rdfs_range,uri_rdfs_comment,X0) ) ).
cnf(u1489,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u2897,axiom,
iext(uri_rdfs_range,X0,uri_rdf_Property) ).
cnf(u358,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| ~ icext(X2,sK16(X1,X2,X3))
| icext(X0,X3) ) ).
cnf(u741,axiom,
( lv(sK13(uri_rdf_XMLLiteral,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ) ).
cnf(u1387,axiom,
lv(sK4(uri_rdfs_Literal)) ).
cnf(u369,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).
cnf(u356,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| ~ iext(X1,X3,X4)
| icext(X2,X4)
| ~ icext(X0,X3) ) ).
cnf(u3564,axiom,
( icext(uri_rdf_List,sK14(uri_rdf_rest,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).
cnf(u3187,axiom,
iext(uri_rdfs_subClassOf,sK4(uri_rdfs_Datatype),X0) ).
cnf(u375,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property) ).
cnf(u2424,axiom,
( ~ iext(uri_rdfs_isDefinedBy,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u3561,axiom,
( icext(uri_rdf_List,sK15(uri_owl_intersectionOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_intersectionOf,X0) ) ).
cnf(u1286,axiom,
( ~ iext(uri_rdf_rest,X0,X1)
| icext(uri_rdf_List,X0) ) ).
cnf(u624,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
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(X2,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u3083,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| ~ icext(X0,X1) ) ).
cnf(u3662,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
| icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u1029,axiom,
icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).
cnf(u1290,axiom,
~ iext(uri_rdf_subject,X0,X1) ).
cnf(u1393,axiom,
idc(sK4(uri_rdfs_Datatype)) ).
cnf(u3591,axiom,
( iext(uri_rdfs_member,sK14(uri_rdfs_isDefinedBy,X0),sK15(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,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(X2,X5)
| icext(X0,X5)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u3457,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(u2563,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0) ).
cnf(u3351,axiom,
iext(uri_rdfs_subClassOf,uri_owl_Nothing,X0) ).
cnf(u2595,axiom,
( ~ icext(X1,sK12(X0,X1))
| iext(uri_rdfs_range,X0,X1) ) ).
cnf(u3595,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(u1941,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u3584,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(u386,axiom,
( iext(uri_rdf_type,X0,X1)
| ~ icext(X1,X0) ) ).
cnf(u3601,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(u3998,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK15(uri_rdfs_subClassOf,X1)) ) ).
cnf(u3880,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(u4004,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(u298,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X1) ) ).
cnf(u2585,axiom,
( ~ icext(X1,sK9(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u3869,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(u3636,axiom,
( lv(sK12(uri_rdfs_comment,X0))
| iext(uri_rdfs_range,uri_rdfs_comment,X0) ) ).
cnf(u557,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u296,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_DatatypeProperty)
| iodp(X0) ) ).
cnf(u3503,axiom,
( icext(uri_rdf_List,sK12(uri_rdf_rest,X0))
| iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).
cnf(u2586,axiom,
iext(uri_rdfs_domain,X0,uri_owl_Thing) ).
cnf(u3640,axiom,
( lv(sK12(uri_rdfs_label,X0))
| iext(uri_rdfs_range,uri_rdfs_label,X0) ) ).
cnf(u3997,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK14(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X1)
| icext(sK15(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u2592,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource) ).
cnf(u3887,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(u2609,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3653,axiom,
( icext(uri_rdf_List,sK9(uri_rdf_first,X0))
| iext(uri_rdfs_domain,uri_rdf_first,X0) ) ).
cnf(u3651,axiom,
( icext(sK10(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_domain,uri_owl_complementOf,X0)
| icext(sK9(uri_owl_complementOf,X0),X1) ) ).
cnf(u4001,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,sK15(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_subPropertyOf,sK14(uri_rdfs_subPropertyOf,X0),uri_rdfs_member)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u3510,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| ~ iext(sK12(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u4015,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(X0,X1,X2)
| ~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X1,X2) ) ).
cnf(u313,axiom,
( ~ iext(uri_rdf_type,X0,uri_rdfs_Literal)
| lv(X0) ) ).
cnf(u3654,axiom,
( icext(uri_rdf_List,sK10(uri_rdf_rest,X0))
| iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).
cnf(u3663,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(u3514,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_onProperty,X0))
| iext(uri_rdfs_range,uri_owl_onProperty,X0) ) ).
cnf(u3660,axiom,
( ~ iext(uri_owl_allValuesFrom,sK9(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_domain,uri_owl_onProperty,X0)
| iext(sK10(uri_owl_onProperty,X0),X2,sK16(sK10(uri_owl_onProperty,X0),X1,X2))
| icext(sK9(uri_owl_onProperty,X0),X2) ) ).
cnf(u364,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).
cnf(u580,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u3524,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(u2895,axiom,
iext(uri_rdfs_range,X0,uri_owl_Thing) ).
cnf(u2004,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u2270,axiom,
( ~ iext(uri_rdf__3,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u3528,axiom,
iext(uri_rdfs_range,uri_rdf_object,X0) ).
cnf(u2770,axiom,
iext(uri_rdfs_subClassOf,uri_owl_AnnotationProperty,X0) ).
cnf(u353,axiom,
( ~ iext(uri_rdfs_subPropertyOf,X0,X1)
| iext(X1,X2,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u3009,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(u2387,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u2267,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,X2)
| ~ iext(X2,X0,X1)
| iext(uri_rdfs_member,X0,X1) ) ).
cnf(u742,axiom,
( lv(sK13(uri_rdfs_Literal,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0) ) ).
cnf(u359,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_hasValue,X0,X2)
| ~ iext(X1,X3,X2)
| icext(X0,X3) ) ).
cnf(u2522,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u602,axiom,
( icext(uri_rdfs_Literal,sK13(uri_rdf_XMLLiteral,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0) ) ).
cnf(u1889,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u2764,axiom,
iext(uri_rdfs_subClassOf,uri_owl_DatatypeProperty,X0) ).
cnf(u357,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_allValuesFrom,X0,X2)
| iext(X1,X3,sK16(X1,X2,X3))
| icext(X0,X3) ) ).
cnf(u3565,axiom,
( icext(uri_rdf_List,sK15(uri_owl_unionOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_unionOf,X0) ) ).
cnf(u1768,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq) ) ).
cnf(u438,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X0,X1)
| iext(uri_rdfs_subClassOf,X0,X2) ) ).
cnf(u2271,axiom,
( ~ iext(sK4(uri_rdfs_ContainerMembershipProperty),X0,X1)
| iext(uri_rdfs_member,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(u370,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).
cnf(u3569,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| iext(sK15(uri_owl_onProperty,X0),X2,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
| icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u2564,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,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(X4,X5)
| ~ icext(X2,X5)
| icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3571,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| ~ icext(X1,sK16(sK15(uri_owl_onProperty,X0),X1,X2))
| icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u1925,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u520,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u498,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_owl_Nothing)
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,X1,X0) ) ).
cnf(u3585,axiom,
( iext(uri_rdfs_member,sK14(uri_rdf__1,X0),sK15(uri_rdf__1,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0) ) ).
cnf(u3864,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(u1285,axiom,
( ~ iext(uri_rdf_first,X0,X1)
| icext(uri_rdf_List,X0) ) ).
cnf(u2588,axiom,
iext(uri_rdfs_domain,X0,uri_rdf_Property) ).
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(X2,X5)
| ~ icext(X0,X5)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u2569,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class) ).
cnf(u1032,axiom,
( icext(uri_rdfs_Literal,sK13(sK13(uri_rdfs_Datatype,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X1)
| iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),X1)
| ~ ic(X0) ) ).
cnf(u387,axiom,
( ~ iext(uri_rdf_type,X0,X1)
| icext(X1,X0) ) ).
cnf(u410,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).
cnf(u2570,axiom,
icext(uri_rdf_Property,X0) ).
cnf(u2452,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u2593,axiom,
iext(uri_rdfs_subClassOf,X0,uri_owl_Thing) ).
cnf(u286,axiom,
( ~ idc(X0)
| ~ icext(X0,X1)
| lv(X1) ) ).
cnf(u2471,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
cnf(u3746,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).
cnf(u3644,axiom,
( lv(sK15(uri_rdfs_comment,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ) ).
cnf(u3752,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).
cnf(u297,axiom,
( ~ ioxp(X0)
| ~ iext(X0,X1,X2)
| ix(X2) ) ).
cnf(u3498,axiom,
( iext(uri_rdf_type,sK13(uri_owl_Ontology,X0),uri_owl_Ontology)
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u1689,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u3706,axiom,
( lv(sK10(uri_rdfs_comment,X0))
| iext(uri_rdfs_domain,uri_rdfs_comment,X0) ) ).
cnf(u3508,axiom,
( icext(uri_owl_Restriction,sK11(uri_owl_hasValue,X0))
| iext(uri_rdfs_range,uri_owl_hasValue,X0) ) ).
cnf(u3909,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(u3907,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(u3512,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(u3913,axiom,
( ~ iext(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1,X2)
| iext(uri_rdfs_member,X1,X2)
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0) ) ).
cnf(u1723,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_List) ) ).
cnf(u3526,axiom,
( iext(uri_rdfs_member,sK11(uri_rdf__2,X0),sK12(uri_rdf__2,X0))
| iext(uri_rdfs_range,uri_rdf__2,X0) ) ).
cnf(u591,axiom,
( ~ icext(uri_rdf_XMLLiteral,X0)
| icext(uri_rdfs_Literal,X0) ) ).
cnf(u324,axiom,
( ~ iext(uri_owl_intersectionOf,X0,X1)
| icext(uri_rdf_List,X1) ) ).
cnf(u3532,axiom,
( iext(uri_rdfs_seeAlso,sK11(uri_rdfs_isDefinedBy,X0),sK12(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_range,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u3525,axiom,
( iext(uri_rdfs_member,sK11(uri_rdf__1,X0),sK12(uri_rdf__1,X0))
| iext(uri_rdfs_range,uri_rdf__1,X0) ) ).
cnf(u343,axiom,
( ~ iext(uri_rdfs_range,X0,X1)
| icext(X1,X3)
| ~ iext(X0,X2,X3) ) ).
cnf(u2506,axiom,
( iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral)
| ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u3568,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_hasValue,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_hasValue,X0) ) ).
cnf(u3916,axiom,
( iext(uri_rdfs_member,sK9(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK10(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_domain,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u3581,axiom,
( ~ icext(sK14(uri_rdfs_subClassOf,X0),X1)
| icext(sK15(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u3529,axiom,
iext(uri_rdfs_range,uri_rdf_subject,X0) ).
cnf(u1382,axiom,
( ~ iext(uri_rdfs_label,X1,X0)
| icext(uri_rdfs_Literal,X0) ) ).
cnf(u1759,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
cnf(u2765,axiom,
~ icext(uri_owl_AnnotationProperty,X0) ).
cnf(u3272,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| ~ icext(X0,X1) ) ).
cnf(u2138,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_ContainerMembershipProperty) ) ).
cnf(u2265,axiom,
( ~ iext(uri_rdfs_isDefinedBy,X0,X1)
| iext(uri_rdfs_seeAlso,X0,X1) ) ).
cnf(u3044,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(u3549,axiom,
iext(uri_rdfs_range,uri_owl_unionOf,uri_rdf_List) ).
cnf(u3673,axiom,
( iext(uri_rdfs_subClassOf,X1,sK10(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK9(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,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(X2,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u383,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).
cnf(u2676,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u212,axiom,
( ~ iext(uri_owl_complementOf,X0,X1)
| ~ icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u3674,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(u1508,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype) ) ).
cnf(u3691,axiom,
iext(uri_rdfs_domain,uri_owl_allValuesFrom,uri_owl_Restriction) ).
cnf(u381,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).
cnf(u3842,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(u3680,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,X0) ).
cnf(u3697,axiom,
iext(uri_rdfs_domain,uri_owl_onProperty,uri_owl_Restriction) ).
cnf(u2566,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0) ).
cnf(u1037,axiom,
( iext(uri_rdfs_subClassOf,sK13(uri_rdfs_Datatype,X0),uri_rdfs_Literal)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| ~ ic(X0) ) ).
cnf(u2928,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(u3711,axiom,
( icext(uri_owl_Ontology,sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u1292,axiom,
~ iext(uri_rdf_object,X0,X1) ).
cnf(u371,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).
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(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u1041,axiom,
( ~ icext(sK13(uri_rdfs_Datatype,X0),X1)
| ~ ic(X0)
| icext(uri_rdfs_Literal,X1)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0) ) ).
cnf(u252,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(u3579,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(u2567,axiom,
( icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
cnf(u3621,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(u3582,axiom,
( iext(uri_rdfs_subClassOf,X1,sK15(uri_rdfs_subClassOf,X0))
| ~ iext(uri_rdfs_subClassOf,X1,sK14(uri_rdfs_subClassOf,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0) ) ).
cnf(u3855,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(u2577,axiom,
iext(uri_rdfs_subClassOf,X0,uri_rdf_Property) ).
cnf(u392,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).
cnf(u3628,axiom,
iext(uri_rdfs_subPropertyOf,X0,X0) ).
cnf(u3747,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ) ).
cnf(u1545,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u411,axiom,
( ~ icext(uri_rdfs_Datatype,X0)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u3893,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(u3891,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(u3914,axiom,
( iext(uri_rdfs_member,sK11(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1),sK12(sK13(uri_rdfs_ContainerMembershipProperty,X0),X1))
| iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0)
| iext(uri_rdfs_range,sK13(uri_rdfs_ContainerMembershipProperty,X0),X1) ) ).
cnf(u1562,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt) ) ).
cnf(u409,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).
cnf(u310,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_Ontology)
| ix(X0) ) ).
cnf(u4021,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X1)
| icext(sK10(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u3496,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(u4025,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(u1598,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral) ) ).
cnf(u3516,axiom,
( ~ iext(uri_owl_onProperty,sK11(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| iext(X1,X2,sK17(X1,sK12(uri_owl_someValuesFrom,X0),X2))
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u1454,axiom,
~ icext(sK4(uri_rdfs_Datatype),X0) ).
cnf(u3509,axiom,
( ~ iext(uri_owl_allValuesFrom,sK11(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_range,uri_owl_onProperty,X0)
| iext(sK12(uri_owl_onProperty,X0),X2,sK16(sK12(uri_owl_onProperty,X0),X1,X2))
| icext(sK11(uri_owl_onProperty,X0),X2) ) ).
cnf(u4008,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(u3513,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(u2423,axiom,
( ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0)
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u4022,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK9(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_domain,uri_rdfs_subClassOf,X1)
| ~ iext(uri_rdfs_subClassOf,X2,X0)
| iext(uri_rdfs_subClassOf,X2,sK10(uri_rdfs_subClassOf,X1)) ) ).
cnf(u1732,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt) ) ).
cnf(u348,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,X1)
| icext(X1,X2)
| ~ icext(X0,X2) ) ).
cnf(u3533,axiom,
( icext(uri_rdfs_Literal,sK12(uri_rdfs_label,X0))
| iext(uri_rdfs_range,uri_rdfs_label,X0) ) ).
cnf(u3657,axiom,
( icext(sK10(uri_rdf_type,X0),sK9(uri_rdf_type,X0))
| iext(uri_rdfs_domain,uri_rdf_type,X0) ) ).
cnf(u367,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).
cnf(u3671,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(u338,axiom,
( ~ iext(uri_rdfs_domain,X0,X1)
| icext(X1,X2)
| ~ iext(X0,X2,X3) ) ).
cnf(u3851,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(u3779,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| ~ iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3677,axiom,
( iext(uri_rdfs_member,sK9(uri_rdf__2,X0),sK10(uri_rdf__2,X0))
| iext(uri_rdfs_domain,uri_rdf__2,X0) ) ).
cnf(u1368,axiom,
( ~ iext(uri_rdf_rest,X1,X0)
| icext(uri_rdf_List,X0) ) ).
cnf(u3658,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_domain,uri_owl_allValuesFrom,X0) ) ).
cnf(u211,axiom,
( ~ iext(uri_owl_complementOf,X0,X1)
| icext(X1,X2)
| icext(X0,X2) ) ).
cnf(u365,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).
cnf(u3664,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(u3681,axiom,
( icext(uri_rdfs_Literal,sK10(uri_rdfs_comment,X0))
| iext(uri_rdfs_domain,uri_rdfs_comment,X0) ) ).
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(X6,X7)
| ~ icext(X4,X7)
| ~ icext(X2,X7)
| icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3559,axiom,
( ~ icext(sK15(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_complementOf,X0)
| ~ icext(sK14(uri_owl_complementOf,X0),X1) ) ).
cnf(u3839,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(u378,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).
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(X4,X7)
| ~ icext(X0,X7)
| ~ iext(uri_owl_intersectionOf,X0,X1) ) ).
cnf(u3563,axiom,
( icext(uri_rdf_List,sK15(uri_rdf_rest,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0) ) ).
cnf(u772,axiom,
( icext(uri_rdfs_Literal,sK13(uri_rdfs_Literal,X0))
| iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0)
| ~ ic(X0) ) ).
cnf(u3566,axiom,
( icext(sK15(uri_rdf_type,X0),sK14(uri_rdf_type,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0) ) ).
cnf(u3583,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(u3586,axiom,
( iext(uri_rdfs_member,sK14(uri_rdf__2,X0),sK15(uri_rdf__2,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0) ) ).
cnf(u226,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(u1293,axiom,
~ icext(uri_rdf_Alt,X0) ).
cnf(u3592,axiom,
( iext(uri_rdfs_seeAlso,sK14(uri_rdfs_isDefinedBy,X0),sK15(uri_rdfs_isDefinedBy,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0) ) ).
cnf(u3570,axiom,
( ~ iext(uri_owl_allValuesFrom,sK14(uri_owl_onProperty,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0)
| ~ iext(sK15(uri_owl_onProperty,X0),X2,X3)
| icext(X1,X3)
| ~ icext(sK14(uri_owl_onProperty,X0),X2) ) ).
cnf(u249,axiom,
( ~ ic(X0)
| icext(X0,sK4(X0))
| iext(uri_owl_unionOf,X0,uri_rdf_nil) ) ).
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(X4,X7)
| icext(X0,X7)
| ~ iext(uri_owl_unionOf,X0,X1) ) ).
cnf(u3297,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdfs_Seq) ) ).
cnf(u2794,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_DatatypeProperty)
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u3894,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(u1040,axiom,
( ~ iext(uri_rdfs_subClassOf,X1,sK13(uri_rdfs_Datatype,X0))
| ~ ic(X0)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdfs_Literal) ) ).
cnf(u4095,axiom,
( iext(uri_rdfs_subClassOf,sK10(uri_owl_complementOf,X0),sK10(uri_owl_complementOf,X0))
| iext(uri_rdfs_domain,uri_owl_complementOf,X0) ) ).
cnf(u265,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(u395,axiom,
( iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,X0) ) ).
cnf(u288,axiom,
( ~ iext(uri_rdf_type,X0,uri_rdfs_Datatype)
| idc(X0) ) ).
cnf(u1425,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Datatype))
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u1671,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing) ) ).
cnf(u2833,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK4(uri_rdfs_Class))
| iext(uri_rdfs_subClassOf,X0,X1) ) ).
cnf(u4005,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(u3895,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(u4003,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(u305,axiom,
( iext(uri_rdf_type,X0,uri_rdf_Property)
| ~ ip(X0) ) ).
cnf(u292,axiom,
( ~ iext(uri_rdf_type,X0,uri_owl_AnnotationProperty)
| ioap(X0) ) ).
cnf(u422,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class) ).
cnf(u4023,axiom,
( ~ icext(uri_rdfs_ContainerMembershipProperty,sK10(uri_rdfs_subPropertyOf,X0))
| iext(uri_rdfs_subPropertyOf,sK9(uri_rdfs_subPropertyOf,X0),uri_rdfs_member)
| iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0) ) ).
cnf(u3500,axiom,
( icext(sK12(uri_owl_complementOf,X0),X1)
| iext(uri_rdfs_range,uri_owl_complementOf,X0)
| icext(sK11(uri_owl_complementOf,X0),X1) ) ).
cnf(u2605,axiom,
( iext(X0,sK9(X0,X1),sK10(X0,X1))
| iext(uri_rdfs_domain,X0,X1) ) ).
cnf(u311,axiom,
( ~ ix(X0)
| iext(uri_rdf_type,X0,uri_owl_Ontology) ) ).
cnf(u420,axiom,
( ~ icext(uri_rdfs_Literal,X0)
| lv(X0) ) ).
cnf(u3504,axiom,
( icext(uri_rdf_List,sK11(uri_rdf_rest,X0))
| iext(uri_rdfs_range,uri_rdf_rest,X0) ) ).
cnf(u3992,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,sK11(uri_rdfs_subClassOf,X1))
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X1)
| icext(sK12(uri_rdfs_subClassOf,X1),X2)
| ~ icext(X0,X2) ) ).
cnf(u2095,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal) ) ).
cnf(u3497,axiom,
( ix(sK13(uri_owl_Ontology,X0))
| iext(uri_rdfs_subClassOf,uri_owl_Ontology,X0) ) ).
cnf(u4006,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(u3888,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(u1855,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement) ) ).
cnf(u4012,axiom,
( iext(uri_rdfs_subPropertyOf,sK4(uri_rdfs_ContainerMembershipProperty),X0)
| ~ iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0) ) ).
cnf(u3517,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)
| iext(uri_rdfs_range,uri_owl_someValuesFrom,X0)
| ~ icext(sK11(uri_owl_someValuesFrom,X0),X2) ) ).
cnf(u682,axiom,
icext(uri_rdfs_Resource,X0) ).
cnf(u1969,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt)
| iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag) ) ).
cnf(u4009,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(u437,axiom,
( iext(uri_rdfs_subClassOf,X0,X0)
| ~ ic(X0) ) ).
cnf(u3271,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_owl_Nothing)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_Bag) ) ).
cnf(u3655,axiom,
( icext(uri_rdf_List,sK9(uri_rdf_rest,X0))
| iext(uri_rdfs_domain,uri_rdf_rest,X0) ) ).
cnf(u322,axiom,
( ~ iext(uri_owl_hasValue,X0,X1)
| icext(uri_owl_Restriction,X0) ) ).
cnf(u3521,axiom,
( ~ icext(sK11(uri_rdfs_subClassOf,X0),X1)
| icext(sK12(uri_rdfs_subClassOf,X0),X1)
| iext(uri_rdfs_range,uri_rdfs_subClassOf,X0) ) ).
cnf(u1221,axiom,
lv(sK4(uri_rdf_XMLLiteral)) ).
cnf(u2120,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container) ) ).
cnf(u3523,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(u3575,axiom,
( ~ iext(uri_owl_onProperty,sK14(uri_owl_someValuesFrom,X0),X1)
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0)
| ~ icext(sK15(uri_owl_someValuesFrom,X0),X2)
| ~ iext(X1,X3,X2)
| icext(sK14(uri_owl_someValuesFrom,X0),X3) ) ).
cnf(u3665,axiom,
( icext(uri_owl_Restriction,sK9(uri_owl_onProperty,X0))
| iext(uri_rdfs_domain,uri_owl_onProperty,X0) ) ).
cnf(u2772,axiom,
icext(uri_owl_Ontology,sK4(uri_owl_Ontology)) ).
cnf(u222,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(u2896,axiom,
iext(uri_rdfs_range,X0,uri_rdfs_Class) ).
cnf(u3679,axiom,
iext(uri_rdfs_domain,uri_rdf_object,X0) ).
cnf(u362,axiom,
( ~ iext(uri_owl_someValuesFrom,X0,X2)
| ~ iext(uri_owl_onProperty,X0,X1)
| iext(X1,X3,sK17(X1,X2,X3))
| ~ icext(X0,X3) ) ).
cnf(u3694,axiom,
iext(uri_rdfs_domain,uri_owl_hasValue,uri_owl_Restriction) ).
cnf(u1261,axiom,
~ icext(uri_rdfs_Statement,X0) ).
cnf(u3700,axiom,
iext(uri_rdfs_domain,uri_owl_someValuesFrom,uri_owl_Restriction) ).
cnf(u235,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(u3589,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdf_subject,X0) ).
cnf(u360,axiom,
( ~ iext(uri_owl_onProperty,X0,X1)
| ~ iext(uri_owl_hasValue,X0,X2)
| iext(X1,X3,X2)
| ~ icext(X0,X3) ) ).
cnf(u3567,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_allValuesFrom,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_allValuesFrom,X0) ) ).
cnf(u3587,axiom,
( iext(uri_rdfs_member,sK14(uri_rdf__3,X0),sK15(uri_rdf__3,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0) ) ).
cnf(u2532,axiom,
iext(uri_owl_intersectionOf,uri_rdfs_Resource,uri_rdf_nil) ).
cnf(u3554,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(u3590,axiom,
( icext(uri_rdfs_Literal,sK15(uri_rdfs_comment,X0))
| iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,X0) ) ).
cnf(u366,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).
cnf(u3574,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_onProperty,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0) ) ).
cnf(u4079,axiom,
( iext(uri_rdfs_subClassOf,sK12(uri_owl_complementOf,X0),sK12(uri_owl_complementOf,X0))
| iext(uri_rdfs_range,uri_owl_complementOf,X0) ) ).
cnf(u3186,axiom,
( ~ iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement)
| ~ iext(uri_rdfs_subClassOf,X1,X0)
| iext(uri_rdfs_subClassOf,X1,uri_rdf_XMLLiteral) ) ).
cnf(u3578,axiom,
( icext(uri_owl_Restriction,sK14(uri_owl_someValuesFrom,X0))
| iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0) ) ).
cnf(u3884,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(u3859,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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB032+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n013.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Mon Sep 28 07:09:22 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 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.92/0.62 % (994988)Will run a generic schedule for satisfiability detection.
% 0.92/0.62 % (994995)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4008769776:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.92/0.62 % (994994)% WARNING: option uhcvi not known.
% 0.92/0.62 % (994993)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=659043037_2999 on theBenchmark for (2999ds/0Mi)
% 0.92/0.62 % (994994)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=671958064:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.92/0.62 % (994996)dis+10_1_sil=32000:sp=arity:random_seed=3249516513:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.92/0.62 % (994997)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3635208568:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.92/0.62 % (994998)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2855328123:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.92/0.62 % (994999)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2010264145:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.92/0.62 % TRYING [1]
% 0.92/0.62 % TRYING [2]
% 0.92/0.62 % TRYING [3]
% 0.92/0.62 % (994997)Instruction limit reached!
% 0.92/0.62 % (994997)------------------------------
% 0.92/0.62 % (994997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (994997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (994997)CaDiCaL version: 2.1.3
% 0.92/0.62 % (994997)Termination reason: Instruction limit
% 0.92/0.62 % (994997)Termination phase: Saturation
% 0.92/0.62 % (994997)Time elapsed: 0.049 s
% 0.92/0.62 % (994997)Peak memory usage: 12 MB
% 0.92/0.62 % (994997)Instructions burned: 117 (million)
% 0.92/0.62 % TRYING [4]
% 0.92/0.62 % (994996)Instruction limit reached!
% 0.92/0.62 % (994996)------------------------------
% 0.92/0.62 % (994996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (994996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (994996)CaDiCaL version: 2.1.3
% 0.92/0.62 % (994996)Termination reason: Instruction limit
% 0.92/0.62 % (994996)Termination phase: Saturation
% 0.92/0.62 % (994996)Time elapsed: 0.061 s
% 0.92/0.62 % (994996)Peak memory usage: 13 MB
% 0.92/0.62 % (994996)Instructions burned: 103 (million)
% 0.92/0.62 % (994998)Instruction limit reached!
% 0.92/0.62 % (994998)------------------------------
% 0.92/0.62 % (994998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (994998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (994998)CaDiCaL version: 2.1.3
% 0.92/0.62 % (994998)Termination reason: Instruction limit
% 0.92/0.62 % (994998)Termination phase: Saturation
% 0.92/0.62 % (994998)Time elapsed: 0.068 s
% 0.92/0.62 % (994998)Peak memory usage: 13 MB
% 0.92/0.62 % (994998)Instructions burned: 132 (million)
% 0.92/0.62 % (995007)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3148409437:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.92/0.62 % (995008)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1151221129:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.92/0.62 % TRYING [1]
% 0.92/0.62 % TRYING [2]
% 0.92/0.62 % TRYING [3]
% 0.92/0.62 % (995009)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=2690719557:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 0.92/0.62 % (994999)Instruction limit reached!
% 0.92/0.62 % (994999)------------------------------
% 0.92/0.62 % (994999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (994999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (994999)CaDiCaL version: 2.1.3
% 0.92/0.62 % (994999)Termination reason: Instruction limit
% 0.92/0.62 % (994999)Termination phase: Saturation
% 0.92/0.62 % (994999)Time elapsed: 0.092 s
% 0.92/0.62 % (994999)Peak memory usage: 15 MB
% 0.92/0.62 % (994999)Instructions burned: 160 (million)
% 0.92/0.62 % (995013)ott-21_1_sil=16000:fs=off:random_seed=2348596133:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.92/0.62 % TRYING [4]
% 0.92/0.62 % (995008)Instruction limit reached!
% 0.92/0.62 % (995008)------------------------------
% 0.92/0.62 % (995008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (995008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (995008)CaDiCaL version: 2.1.3
% 0.92/0.62 % (995008)Termination reason: Instruction limit
% 0.92/0.62 % (995008)Termination phase: Saturation
% 0.92/0.62 % (995008)Time elapsed: 0.064 s
% 0.92/0.62 % (995008)Peak memory usage: 13 MB
% 0.92/0.62 % (995008)Instructions burned: 131 (million)
% 0.92/0.62 % (995009) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-994988-995009"...
% 0.92/0.62 % (995009)...printing done.
% 0.92/0.62 % SZS status CounterSatisfiable for theBenchmark
% 0.92/0.62 % SZS output start Saturation.
% See solution above
% 0.92/0.62 % SZS output start Definitions and Model Updates.
% 0.92/0.62 for all groundings,
% 0.92/0.62 whenever iext(uri_rdf_type,X0,uri_rdfs_Datatype) is false, set ~idc(X0) to true
% 0.92/0.62 for all groundings,
% 0.92/0.62 whenever iext(uri_rdf_type,X0,uri_owl_AnnotationProperty) is false, set ~ioap(X0) to true
% 0.92/0.62 for all groundings,
% 0.92/0.62 whenever iext(uri_rdf_type,X0,uri_owl_DatatypeProperty) is false, set ~iodp(X0) to true
% 0.92/0.62 for all groundings,
% 0.92/0.62 whenever iext(uri_rdf_type,X0,uri_owl_OntologyProperty) is false, set ~ioxp(X0) to true
% 0.92/0.62 % SZS output end Definitions and Model Updates.
% 0.92/0.62 % (995009)------------------------------
% 0.92/0.62 % (995009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.92/0.62 % (995009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.92/0.62 % (995009)CaDiCaL version: 2.1.3
% 0.92/0.62 % (995009)Termination reason: Satisfiable
% 0.92/0.62 % (995009)Time elapsed: 0.063 s
% 0.92/0.62 % (995009)Peak memory usage: 14 MB
% 0.92/0.62 % (995009)Instructions burned: 102 (million)
% 0.92/0.62 % (994988)Success in time 0.191 s
% 0.92/0.62 % Vampire exiting
%------------------------------------------------------------------------------