<> <#rcsid> "$Id: owl-rules.n3,v 1.25 2003/09/29 23:24:22 jderoo Exp $". @prefix log: . @prefix math: . @prefix owl: . @prefix xsd: . @prefix rdfs: . @prefix rdf: . @prefix : . ### Web Ontology Language OWL owl:AnnotationProperty rdfs:subClassOf rdf:Property. owl:Class is rdfs:subClassOf of rdfs:Class; rdfs:subClassOf rdfs:Class. owl:DataRange rdfs:subClassOf rdfs:Literal. owl:DatatypeProperty rdfs:subClassOf rdf:Property. owl:DeprecatedClass rdfs:subClassOf rdfs:Class. owl:DeprecatedProperty rdfs:subClassOf rdf:Property. owl:FunctionalProperty rdfs:subClassOf rdf:Property. owl:InverseFunctionalProperty rdfs:subClassOf owl:ObjectProperty. owl:Nothing owl:oneOf rdf:nil. owl:ObjectProperty rdfs:subClassOf rdf:Property. owl:OntologyProperty rdfs:subClassOf rdf:Property. owl:Restriction rdfs:subClassOf owl:Class. owl:SymmetricProperty rdfs:subClassOf owl:ObjectProperty. owl:Thing is rdfs:subClassOf of rdfs:Resource; rdfs:subClassOf rdfs:Resource. owl:TransitiveProperty rdfs:subClassOf owl:ObjectProperty. owl:allValuesFrom rdfs:domain owl:Restriction; rdfs:range rdfs:Class. owl:cardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger; rdfs:subPropertyOf owl:maxCardinality, owl:minCardinality. owl:complementOf rdfs:domain owl:Class; rdfs:range owl:Class; rdfs:subPropertyOf owl:disjointWith; a owl:SymmetricProperty. owl:differentFrom rdfs:domain owl:Thing; rdfs:range owl:Thing; a owl:SymmetricProperty. owl:disjointWith rdfs:domain owl:Class; rdfs:range owl:Class; a owl:SymmetricProperty. owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List. owl:hasValue rdfs:domain owl:Restriction; rdfs:range rdfs:Resource. owl:intersectionOf rdfs:domain owl:Class; rdfs:range rdf:List. owl:inverseOf rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty; a owl:SymmetricProperty. owl:maxCardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger. owl:minCardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger. owl:onProperty rdfs:domain owl:Restriction; rdfs:range rdf:Property. owl:oneOf rdfs:domain rdfs:Class; rdfs:range rdf:List. owl:someValuesFrom rdfs:domain owl:Restriction; rdfs:range rdfs:Class. owl:unionOf rdfs:domain owl:Class; rdfs:range rdf:List. owl:backwardCompatibleWith rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:imports rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:incompatibleWith rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:priorVersion rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:versionInfo rdfs:domain rdfs:Resource; rdfs:range rdfs:Resource; a owl:AnnotationProperty. rdfs:comment a owl:AnnotationProperty. rdfs:isDefinedBy a owl:AnnotationProperty. rdfs:label a owl:AnnotationProperty. rdfs:seeAlso a owl:AnnotationProperty. ### inference rules for Web Ontology Language OWL {:owl1i1. ?P owl:inverseOf ?Q. ?S ?P ?O} => {?O ?Q ?S}. {:owl1s1. ?P a owl:SymmetricProperty. ?S ?P ?O} => {?O ?P ?S}. {:owl2t1. ?P a owl:TransitiveProperty. ?X ?P ?O. ?S ?P ?X} => {?S ?P ?O}. {:owl3r1. ?R owl:onProperty ?P; owl:hasValue ?Y. ?X a ?R} => {?X ?P ?Y}. {:owl6e3. ?P has rdf:type owl:InverseFunctionalProperty. ?X ?P ?O. ?Y ?P ?O} => {?X owl:sameAs ?Y}. {:owl6e2. ?P has rdf:type owl:FunctionalProperty. ?S ?P ?X. ?S ?P ?Y} => {?X owl:sameAs ?Y}. {:owl6x1. ?C1 has owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 has rdfs:domain ?C1; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P9. ?C1 has owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 has rdfs:domain ?C1; has rdfs:range ?C5; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P7. ?C5 has owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 has rdfs:domain ?C5; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P8. ?C5 has owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?X1 has owl:sameAs ?Y1. ?C3 has owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?X2 has owl:sameAs ?Y2. ?C3 has owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?C3 has owl:oneOf ?E. ?E rdf:first ?Z; rdf:rest rdf:nil. (?Y1 ?Y2) math:product ?Z3. ?Z3 math:equalTo ?Y3} => {?X3 owl:sameAs ?Y3}. {:owl6x2. ?C1 has owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 has rdfs:domain ?C1; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P9. ?C1 has owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 has rdfs:domain ?C1; has rdfs:range ?C5; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P7. ?C5 has owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 has rdfs:domain ?C5; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty; owl:inverseOf ?P8. ?C5 has owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?C3 has owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?C3 has owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?X3 has owl:sameAs ?Y3. ?C3 has owl:oneOf ?E. ?E rdf:first ?Z; rdf:rest rdf:nil. ?O has owl:oneOf ?L1. ?L1 :item ?X1, ?X2. ?O has owl:oneOf ?L2. ?L2 :item ?Z1, ?Z2. (?Y3 ?Y2) math:integerQuotient ?Y1} => {?Z2 owl:sameAs ?Y2}. {:owl6d1. ?L rdf:first ?X; rdf:rest ?M. ?M :item ?Y. ?A owl:distinctMembers ?L} => {?X owl:differentFrom ?Y}. {:owl6d2. ?A owl:disjointWith ?B. ?X a ?A. ?Y a ?B } => {?X owl:differentFrom ?Y}. {:owl7p1. ?A rdfs:subPropertyOf ?B. ?B rdfs:subPropertyOf ?A} => {?A owl:equivalentProperty ?B}. {:owl7p2. ?A owl:inverseOf ?C. ?B owl:inverseOf ?C} => {?A rdfs:subPropertyOf ?B}. {:owl7p3. ?A owl:onProperty ?P, ?Q; owl:hasValue ?V. ?P has rdfs:domain ?A; a owl:FunctionalProperty. ?Q rdfs:domain ?D; a owl:FunctionalProperty} => {?P rdfs:subPropertyOf ?Q}. {:owl7p4. ?A owl:onProperty ?P; owl:hasValue ?V. ?D owl:equivalentClass ?A. ?P has rdfs:domain ?D; a owl:FunctionalProperty. ?B owl:onProperty ?Q; owl:hasValue ?V. ?D owl:equivalentClass ?B. ?Q has rdfs:domain ?D; a owl:FunctionalProperty} => {?P rdfs:subPropertyOf ?Q}. {:owl823. ?B owl:onProperty ?P1; owl:someValuesFrom ?X. ?X has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P2; owl:someValuesFrom owl:Thing. ?L :item ?I2. ?I2 owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?L :item ?I3. ?I3 owl:onProperty ?P2; owl:allValuesFrom ?C. ?L :item ?I4. ?I4 owl:onProperty ?P3; owl:allValuesFrom ?U. ?U2 owl:onProperty ?P2; owl:someValuesFrom owl:Thing. ?U has owl:equivalentClass ?U2. ?L :item ?I5. ?I5 owl:onProperty ?P3; owl:allValuesFrom ?V. ?V2 owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?V has owl:equivalentClass ?V2. ?L :item ?I6. ?I6 owl:onProperty ?P3; owl:allValuesFrom ?W. ?W2 owl:onProperty ?P2; owl:allValuesFrom ?C. ?W has owl:equivalentClass ?W2. ?C has owl:equivalentClass ?C1. ?C1 owl:onProperty ?P8; owl:allValuesFrom ?C2. ?P8 owl:inverseOf ?P2. ?D2 owl:onProperty ?P7; owl:allValuesFrom ?C3. ?P7 owl:inverseOf ?P3. ?C2 has owl:equivalentClass ?D2. ?D3 owl:onProperty ?P9; owl:allValuesFrom ?C4. ?P9 owl:inverseOf ?P1. ?C3 has owl:equivalentClass ?D3. ?C4 owl:complementOf ?A. ?P3 a owl:TransitiveProperty. ?D rdfs:subClassOf ?A, ?B} => {?D owl:equivalentClass owl:Nothing}. {:owl830. ?Z has owl:equivalentClass ?J. ?J owl:onProperty ?P1; owl:someValuesFrom ?T. ?T has owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P9; :someOrAll ?G. ?G2 owl:onProperty ?P1; owl:someValuesFrom ?U. ?G has owl:equivalentClass ?G2. ?U owl:complementOf ?I1. ?P1 owl:inverseOf ?P9; a owl:FunctionalProperty} => {?Z owl:equivalentClass owl:Nothing}. {:owl840. ?J has owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I1 has rdfs:subClassOf ?J1. ?J1 owl:onProperty ?P; owl:someValuesFrom ?A1. ?I2 has rdfs:subClassOf ?J2. ?J2 owl:onProperty ?P; owl:allValuesFrom ?A2. ?A1 has rdfs:subClassOf ?C1. ?C1 has owl:intersectionOf ?D1. ?D1 rdf:first ?E1; rdf:rest ?F1. ?F1 rdf:first ?G1; rdf:rest rdf:nil. ?E1 has owl:unionOf ?H1. ?H1 :item ?X1. ?G1 has owl:unionOf ?K1. ?K1 :item ?X1. ?A2 has rdfs:subClassOf ?C2. ?C2 has owl:intersectionOf ?D2. ?D2 rdf:first ?E2; rdf:rest ?F2. ?F2 rdf:first ?G2; rdf:rest rdf:nil. ?E2 has owl:unionOf ?H2. ?H2 :item ?X2. ?G2 has owl:unionOf ?K2. ?K2 :item ?X3. ?X1 owl:complementOf ?X2, ?X3. ?C has rdfs:subClassOf ?J} => {?C owl:equivalentClass owl:Nothing}. {:owl804. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?S. ?L :item ?I2. ?I2 owl:onProperty ?Q; owl:someValuesFrom ?T. ?F owl:onProperty ?P; owl:someValuesFrom ?D. ?D has owl:intersectionOf ?K. ?K :item ?S, ?T. ?L :item ?I3. ?G owl:complementOf ?I3. ?G has owl:equivalentClass ?F. ?P has rdf:type owl:FunctionalProperty; has rdfs:subPropertyOf ?R. ?Q has rdf:type owl:FunctionalProperty; has rdfs:subPropertyOf ?R. ?R has rdf:type owl:FunctionalProperty} => {?J owl:equivalentClass owl:Nothing}. {:owl808. ?J has owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?S. ?S has owl:intersectionOf ?K. ?K :item ?U. ?U owl:onProperty ?Q; owl:someValuesFrom ?Y. ?Q owl:inverseOf ?P. ?K :item ?V. ?V owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 1. ?I1 owl:disjointWith ?Y} => {?J owl:equivalentClass owl:Nothing}. {:owl810. ?J has owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?F; owl:someValuesFrom ?T. ?T has owl:intersectionOf ?K. ?K :item ?G. ?G owl:onProperty ?Q; owl:allValuesFrom ?X. ?K :item ?H. ?H owl:onProperty ?P; owl:allValuesFrom ?U. ?V owl:onProperty ?S; owl:someValuesFrom ?X. ?U has owl:equivalentClass ?V. ?L :item ?I1. ?X owl:complementOf ?I1. ?F has rdf:type owl:FunctionalProperty; owl:inverseOf ?P. ?S has rdf:type owl:FunctionalProperty; owl:inverseOf ?Q; has rdfs:subPropertyOf ?F} => {?J owl:equivalentClass owl:Nothing}. {:owl826. ?J has owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?P9; owl:someValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P8; owl:allValuesFrom ?E. ?E2 owl:onProperty ?P9; owl:someValuesFrom ?D. ?E has owl:equivalentClass ?E2. ?X has owl:intersectionOf ?K. ?D has owl:equivalentClass ?X. ?K :item ?C, ?Y. ?Y owl:onProperty ?P1; owl:someValuesFrom ?Z. ?Z owl:complementOf ?C. ?L :item ?I1. ?I1 owl:complementOf ?C. ?P9 owl:inverseOf ?P1. ?P8 owl:inverseOf ?P2. ?P2 a owl:TransitiveProperty. ?P1 rdfs:subPropertyOf ?P2; a owl:FunctionalProperty} => {?J owl:equivalentClass owl:Nothing}. {:owl829. ?J has owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P1; owl:someValuesFrom ?S. ?S2 owl:onProperty ?P1; owl:someValuesFrom ?T. ?S has owl:equivalentClass ?S2. ?T has owl:intersectionOf ?K. ?K :item ?I1, ?I3. ?I3 owl:onProperty ?P9; owl:allValuesFrom ?U. ?U owl:complementOf ?I1. ?P1 owl:inverseOf ?P9; a owl:TransitiveProperty} => {?J owl:equivalentClass owl:Nothing}. {:owl850. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?B. ?B owl:complementOf ?E. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?U. ?U has owl:unionOf ?K. ?K :item ?E, ?Y. ?Y owl:complementOf ?D} => {?J owl:equivalentClass owl:Nothing}. {:owl851. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?B. ?B owl:complementOf ?E. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?U. ?U2 has owl:intersectionOf ?K. ?U2 owl:complementOf ?U. ?K :item ?D, ?Y. ?Y owl:complementOf ?E} => {?J owl:equivalentClass owl:Nothing}. {:owl805. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1} => {?J owl:equivalentClass owl:Nothing}. {:owl806. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1} => {?J owl:equivalentClass owl:Nothing}. {:owl807. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 2. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2} => {?J owl:equivalentClass owl:Nothing}. {:owl819. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 3. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?C4. ?C4 owl:disjointWith ?C1, ?C2, ?C3} => {?J owl:equivalentClass owl:Nothing}. {:owl822. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 4. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?C4. ?C4 owl:disjointWith ?C1, ?C2, ?C3. ?L :item ?I5. ?I5 owl:onProperty ?P; owl:someValuesFrom ?C5. ?C5 owl:disjointWith ?C1, ?C2, ?C3, ?C4} => {?J owl:equivalentClass owl:Nothing}. {:owl803. ?C has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P3; owl:someValuesFrom ?C3. ?P1 a owl:FunctionalProperty. ?P2 a owl:FunctionalProperty. ?P3 rdfs:subPropertyOf ?P1, ?P2} => {?C owl:equivalentClass owl:Nothing}. {:owl811. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:allValuesFrom ?S. ?S owl:complementOf ?G. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?T. ?T has owl:intersectionOf ?K. ?K :item ?F. ?F owl:onProperty ?Q; owl:someValuesFrom ?G. ?K :item ?G. ?P has rdf:type owl:FunctionalProperty. ?Q owl:inverseOf ?P} => {?J owl:equivalentClass owl:Nothing}. {:owl813. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?T. ?T has owl:intersectionOf ?K. ?K :item ?X. ?X owl:complementOf ?C1. ?K :item ?H. ?H owl:onProperty ?P8; owl:allValuesFrom ?V. ?U owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?V has owl:equivalentClass ?U. ?P1 a owl:FunctionalProperty. ?P2 a owl:FunctionalProperty; owl:inverseOf ?P8. ?P3 a owl:FunctionalProperty; rdfs:subPropertyOf ?P1, ?P2} => {?J owl:equivalentClass owl:Nothing}. {:owl814. ?J has owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?F; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I3. ?I3 owl:onProperty ?F; owl:someValuesFrom ?T. ?U owl:onProperty ?Q; owl:allValuesFrom ?X. ?T has owl:equivalentClass ?U. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?X. ?L :item ?I1. ?I1 owl:complementOf ?X. ?Q owl:inverseOf ?P. ?P rdfs:subPropertyOf ?F} => {?J owl:equivalentClass owl:Nothing}. {:owl815. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?S. ?S has owl:intersectionOf ?K. ?K :item ?U. ?U owl:complementOf ?C1. ?K :item ?V. ?V owl:complementOf ?C2. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?T. ?T has owl:intersectionOf ?O. ?O :item ?G. ?G owl:onProperty ?P8; owl:maxCardinality ?M. ?M math:equalTo 1. ?O :item ?H. ?H owl:onProperty ?P8; owl:someValuesFrom ?W. ?X owl:onProperty ?P1; owl:allValuesFrom ?C1. ?W has owl:equivalentClass ?X. ?P2 owl:inverseOf ?P8} => {?J owl:equivalentClass owl:Nothing}. {:owl835. ?A owl:onProperty ?X; owl:minCardinality ?N. ?N math:greaterThan 2. owl:Thing has rdfs:subClassOf ?B. ?B owl:onProperty ?P; owl:someValuesFrom ?O. ?O owl:oneOf ?L. ?L rdf:first ?S; rdf:rest rdf:nil. ?S has rdf:type ?D. ?D owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 2. ?Q owl:inverseOf ?P. ?C rdfs:subClassOf ?A} => {?C owl:equivalentClass owl:Nothing}. {:owl898. ?Z has owl:equivalentClass ?J. ?J has owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?C1 has owl:intersectionOf ?K1. ?K1 :item ?X1. ?X1 owl:onProperty ?T; owl:maxCardinality ?M1. ?M1 math:equalTo 1. ?K1 :item ?X2. ?X2 owl:onProperty ?T1; owl:someValuesFrom ?D1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?C2. ?C2 has owl:intersectionOf ?K2. ?K2 :item ?Y1. ?Y1 owl:onProperty ?T; owl:maxCardinality ?M2. ?M2 math:equalTo 1. ?K2 :item ?Y2. ?Y2 owl:onProperty ?T2; owl:someValuesFrom ?D2. ?D2 owl:disjointWith ?D1. ?P1 rdfs:subPropertyOf ?P. ?P2 rdfs:subPropertyOf ?P. ?T1 rdfs:subPropertyOf ?T. ?T2 rdfs:subPropertyOf ?T} => {?Z owl:equivalentClass owl:Nothing}. {:owl891. ?J has owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:onProperty ?Q; owl:minCardinality ?N. ?N math:equalTo 2. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?A. ?A has owl:unionOf ?K. ?K :item ?C, ?V. ?V owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?D. ?C owl:disjointWith ?D} => {?J owl:equivalentClass owl:Nothing}. {:owl889. ?C1 has owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C6. ?P1 has rdfs:domain ?C1; has rdfs:range ?C6; has rdf:type owl:FunctionalProperty. ?C1 has owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 has rdfs:domain ?C1; has rdfs:range ?C5; has rdf:type owl:FunctionalProperty. ?C5 has owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C6. ?P2 has rdfs:domain ?C5; has rdfs:range ?C6; has rdf:type owl:FunctionalProperty. ?C5 has owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?P7 owl:inverseOf ?P3. ?C6 has owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?P8 owl:inverseOf ?P2. ?C6 has owl:equivalentClass ?H. ?H owl:onProperty ?P9; owl:cardinality ?X3. ?P9 owl:inverseOf ?P1. ?H has owl:equivalentClass ?I. ?I owl:onProperty ?P4; owl:someValuesFrom ?C3. ?P4 has rdfs:domain ?C6; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty. ?C3 has owl:equivalentClass ?G. ?G owl:onProperty ?P6; owl:maxCardinality ?X4. ?P6 owl:inverseOf ?P4. (?X1 ?X2) math:product ?X. ?X math:notEqualTo ?X3} => {?C3 owl:equivalentClass owl:Nothing}. {:owl880. ?C1 has owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 has rdfs:domain ?C1; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty. ?C1 has owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 has rdfs:domain ?C1; has rdfs:range ?C5; has rdf:type owl:FunctionalProperty. ?C5 has owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 has rdfs:domain ?C5; has rdfs:range ?C3; has rdf:type owl:FunctionalProperty. ?C5 has owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?P7 owl:inverseOf ?P3. ?C3 has owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?P8 owl:inverseOf ?P2. ?C3 has owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?P9 owl:inverseOf ?P1. (?X1 ?X2) math:product ?X. ?X math:notEqualTo ?X3} => {?C3 owl:equivalentClass owl:Nothing}. {:owl8u1. ?D has owl:equivalentClass ?C. ?C has owl:unionOf ?L. ?L :allClasses owl:Nothing} => {?D owl:equivalentClass owl:Nothing}. {:owl8i1. ?D owl:complementOf ?C. ?C has owl:intersectionOf ?L. ?L :allClasses owl:Thing} => {?D owl:equivalentClass owl:Nothing}. {:owl8i2. ?C has owl:intersectionOf ?L. ?L :item ?A, ?B. ?A owl:disjointWith ?B} => {?C owl:equivalentClass owl:Nothing}. {:owl8i3. ?C has owl:intersectionOf ?L. ?L :item owl:Nothing} => {?C owl:equivalentClass owl:Nothing}. {:owl8e1. ?A owl:onProperty ?P; owl:maxCardinality ?M. ?B owl:onProperty ?P; owl:minCardinality ?N. ?M math:lessThan ?N. ?C rdfs:subClassOf ?A, ?B} => {?C owl:equivalentClass owl:Nothing}. {:owl8t1. ?D owl:complementOf ?C. ?D owl:equivalentClass owl:Nothing} => {?C owl:equivalentClass owl:Thing}. {:owl8t2. ?C has owl:unionOf ?L. ?L :item owl:Thing} => {?C owl:equivalentClass owl:Thing}. {:owl8m1. ?D has owl:intersectionOf ?L3. ?L3 rdf:first ?X; rdf:rest ?L4. ?L4 rdf:first ?Y; rdf:rest rdf:nil. ?X owl:complementOf ?A. ?Y owl:complementOf ?B. ?Z owl:complementOf ?C. ?C has owl:unionOf ?L1. ?L1 rdf:first ?A; rdf:rest ?L2. ?L2 rdf:first ?B; rdf:rest rdf:nil} => {?D owl:equivalentClass ?Z}. {:owl8m2. ?D has owl:unionOf ?L3. ?L3 rdf:first ?X; rdf:rest ?L4. ?L4 rdf:first ?Y; rdf:rest rdf:nil. ?X owl:complementOf ?A. ?Y owl:complementOf ?B. ?Z owl:complementOf ?C. ?C has owl:intersectionOf ?L1. ?L1 rdf:first ?A; rdf:rest ?L2. ?L2 rdf:first ?B; rdf:rest rdf:nil} => {?D owl:equivalentClass ?Z}. {:owl8c1. ?A rdfs:subClassOf ?B. ?B rdfs:subClassOf ?A} => {?A owl:equivalentClass ?B}. {:owl8c4. ?B has owl:intersectionOf ?L. ?L rdf:first ?A; rdf:rest rdf:nil} => {?A rdfs:subClassOf ?B}. {:owl8s4. ?A owl:intersectionOf ?X. ?X :item ?B} => {?A rdfs:subClassOf ?B}. {:owl8s1. ?B has owl:intersectionOf ?Y. ?A has owl:intersectionOf ?X. ?X :includes ?Y} => {?A rdfs:subClassOf ?B}. {:owl8s2. ?B has owl:unionOf ?Y. ?A has owl:unionOf ?X. ?Y :includes ?X} => {?A rdfs:subClassOf ?B}. {:owl8s3. ?B has owl:oneOf ?Y. ?A has owl:oneOf ?X. ?Y :includes ?X} => {?A rdfs:subClassOf ?B}. {:owl8s6. ?R owl:onProperty ?P; owl:allValuesFrom ?A. ?S owl:onProperty ?P; owl:allValuesFrom ?A} => {?R rdfs:subClassOf ?S}. {:owl8s7. ?A owl:onProperty rdf:type; owl:hasValue ?B} => {?A rdfs:subClassOf ?B}. {:owl8s8. ?R owl:onProperty ?P; owl:minCardinality ?M. ?S owl:onProperty ?P; owl:maxCardinality ?M. ?T owl:onProperty ?P; owl:cardinality ?M. ?C rdfs:subClassOf ?R, ?S} => {?C rdfs:subClassOf ?T}. {:owl8y1. ?X has owl:intersectionOf ?L. ?L :item ?U. ?U owl:onProperty ?P; owl:minCardinality ?I. ?L :item ?V. ?V owl:onProperty ?Q; owl:minCardinality ?J. ?Y owl:onProperty ?R; owl:minCardinality ?K. (?I ?J) math:sum ?G. ?G math:equalTo ?K. ?P has rdfs:subPropertyOf ?R; has rdfs:range ?A. ?Q has rdfs:subPropertyOf ?R; has rdfs:range ?B. ?A owl:disjointWith ?B} => {?X rdfs:subClassOf ?Y}. {:owl8x0. ?R owl:onProperty ?P; owl:allValuesFrom ?A. ?P rdfs:range ?A} => {owl:Thing rdfs:subClassOf ?R}. {:owl8x1. rdf:type rdfs:domain ?Y. ?X a rdfs:Class} => {?X rdfs:subClassOf ?Y}. {:owl9f0. owl:Thing has rdfs:subClassOf ?U. ?U owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1} => {?P a owl:FunctionalProperty}. {:owl9f1. ?P owl:inverseOf ?Q. ?Q a owl:FunctionalProperty} => {?P a owl:InverseFunctionalProperty}. {:owl9f2. ?C has owl:oneOf ?L. ?L rdf:first ?X; rdf:rest rdf:nil. ?P has rdfs:range ?C} => {?P a owl:FunctionalProperty}. {:owl9v1. ?P owl:inverseOf ?Q. ?Q a owl:InverseFunctionalProperty} => {?P a owl:FunctionalProperty}. {:owl9v2. ?C has owl:oneOf ?L. ?L rdf:first ?X; rdf:rest rdf:nil. ?P has rdfs:domain ?C} => {?P a owl:InverseFunctionalProperty}. {:owl9s1. ?P has rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?D owl:oneOf ?A. ?A :includes ?B. ?P has a owl:InverseFunctionalProperty} => {?P a owl:SymmetricProperty}. {:owl9t1. ?P has rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?P has a owl:SymmetricProperty} => {?P a owl:TransitiveProperty}. {:owl9r0. ?C has owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:someValuesFrom ?A. ?X ?P ?Y. ?Y a ?A} => {?X a ?C}. {:owl9o1. ?C has owl:oneOf ?L. ?L :item ?X} => {?X a ?C}. {:owl9i2. ?C has owl:intersectionOf ?L. ?X :inAllOf ?L} => {?X a ?C}. {:owl9i3. ?C has owl:equivalentClass ?D. ?D has owl:intersectionOf ?L. ?X :inAllOf ?L} => {?X a ?C}. {:owl9u1. ?C has owl:unionOf ?L. ?X :inSomeOf ?L} => {?X a ?C}. {:owl9u2. ?C has owl:unionOf ?L. ?L :item ?A, ?B. ?A owl:complementOf ?B} => {?X a ?C}. {:owl9u3. ?C has owl:unionOf ?L. ?L :item ?A, ?B. ?A owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?B owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0} => {?X a ?C}. {:owl9x1. ?R owl:onProperty ?P; owl:allValuesFrom ?A. ?S owl:onProperty ?P; owl:allValuesFrom ?A. ?X has rdf:type ?R} => {?X a ?S}. {:owl9c0. ?C has owl:complementOf ?A. ?B has owl:complementOf ?A. ?X has rdf:type ?C} => {?X a ?B}. {:owl9r1. ?R owl:onProperty ?P; owl:allValuesFrom ?A. ?X ?P ?Y; a ?R} => {?Y a ?A}. {:owl9r2. ?R owl:onProperty ?P; owl:hasValue ?Y. ?X ?P ?Y} => {?X a ?R}. {:owl9r3. ?R owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?P owl:inverseOf ?Q; rdfs:range ?O. ?Y ?Q ?X; a ?O} => {?X a ?R}. {:owl9r4. ?R owl:onProperty ?P; owl:someValuesFrom ?A. ?X ?P ?Y. ?Y a ?A} => {?X a ?R}. {:owl9r5. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?P a owl:FunctionalProperty} => {?X a ?R}. {:owl9r6. ?R owl:onProperty ?P; owl:minCardinality ?M. ?M math:equalTo 1. ?P has rdfs:range ?A. ?A owl:oneOf ?B. ?P :reflexive ?B. ?P has a owl:SymmetricProperty} => {?X a ?R}. {:owl10a1. ?L rdf:rest ?M. ?A owl:distinctMembers ?L} => {?A owl:distinctMembers ?M}. {:owl10a2. ?R owl:onProperty ?P; owl:minCardinality ?M. ?P has rdfs:range ?X. ?X has owl:oneOf ?L. ?L :memberCount ?N. ?M math:notLessThan ?N} => {?X owl:distinctMembers ?L}. {:owl10d1. ?A has rdfs:subClassOf ?C. ?B owl:complementOf ?C} => {?B owl:disjointWith ?A}. {:owl10x1. ?A has rdfs:subClassOf ?C. ?C has owl:intersectionOf ?L. ?L :item ?I. ?B owl:complementOf ?I} => {?A owl:disjointWith ?B}. {:owl10d2. ?A has rdfs:subClassOf ?C. ?C has owl:complementOf ?D. ?D has owl:unionOf ?L. ?L :item ?B} => {?A owl:disjointWith ?B}. {:owl10d3. ?T owl:onProperty ?P; owl:cardinality ?M. ?M math:equalTo 1. ?C has rdfs:subClassOf ?T. ?A has rdfs:subClassOf ?C; has rdfs:subClassOf ?R. ?R owl:onProperty ?P; owl:hasValue ?V. ?B has rdfs:subClassOf ?C; has rdfs:subClassOf ?S. ?S owl:onProperty ?P; owl:hasValue ?W} => {?A owl:disjointWith ?B}. {:owl10x2. ?R owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?S owl:onProperty ?P; owl:allValuesFrom ?D. ?D owl:equivalentClass owl:Nothing. ?E rdfs:subClassOf ?R, ?S} => {?R owl:disjointWith ?S}. {:owl11d1. ?P has rdfs:domain ?C. ?C has rdfs:subClassOf ?D} => {?P rdfs:domain ?D}. {:owl11d2. ?P owl:inverseOf ?Q. ?P has rdfs:range ?C} => {?Q rdfs:domain ?C}. {:owl11d3. ?P has rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?D owl:oneOf ?A. ?A :includes ?B. ?P has a owl:InverseFunctionalProperty} => {?P rdfs:domain ?D}. {:owl11r1. ?P has rdfs:range ?C. ?C has rdfs:subClassOf ?D} => {?P rdfs:range ?D}. {:owl11r2. ?P owl:inverseOf ?Q. ?P has rdfs:domain ?C} => {?Q rdfs:range ?C}. {:owl11r3. ?R owl:onProperty ?P; owl:allValuesFrom ?A. owl:Thing rdfs:subClassOf ?R} => {?P rdfs:range ?A}. {:owl11r4. ?P has rdfs:range ?C; has rdfs:range ?D. ?E has owl:intersectionOf ?L. ?L :item ?C, ?D} => {?P rdfs:range ?E}. {:owl12c1. ?A has owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:someValuesFrom ?C. ?C owl:equivalentClass owl:Thing. ?B has owl:equivalentClass ?S. ?S owl:onProperty ?P; owl:allValuesFrom ?D. ?D owl:equivalentClass owl:Nothing} => {?A owl:complementOf ?B}. {:owl12c2. ?A has owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:minCardinality ?N. ?B has owl:equivalentClass ?S. ?S owl:onProperty ?P; owl:maxCardinality ?M. ?M math:lessThan ?N} => {?A owl:complementOf ?B}. {:owl13u0. ?U owl:complementOf ?V. ?V has owl:intersectionOf ?K. ?K rdf:first ?X; rdf:rest ?K1. ?K1 rdf:first ?Y; rdf:rest rdf:nil. ?A owl:complementOf ?X. ?L rdf:first ?A; rdf:rest ?L1. ?L1 rdf:first ?B; rdf:rest rdf:nil. ?B owl:complementOf ?Y} => {?U owl:unionOf ?L}. {:owl13u1. ?U owl:complementOf ?V. ?V has owl:intersectionOf ?K. ?K rdf:first ?X; rdf:rest ?K1. ?K1 rdf:first ?Y; rdf:rest rdf:nil. ?A owl:complementOf ?Y. ?L rdf:first ?A; rdf:rest ?L1. ?L1 rdf:first ?B; rdf:rest rdf:nil. ?B owl:complementOf ?X} => {?U owl:unionOf ?L}. {:owl13u2. ?U has owl:oneOf ?K. ?L :ones ?K} => {?U owl:unionOf ?L}. {:owl14i1. ?I owl:complementOf ?V. ?V has owl:unionOf ?K. ?K :item ?X, ?Y. ?A owl:complementOf ?X. ?L :item ?A, ?B. ?B owl:complementOf ?Y} => {?I owl:intersectionOf ?L}. {:owl14i2. ?I has owl:intersectionOf ?K. ?K :item ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?K :item ?S. ?S owl:onProperty ?P; owl:minCardinality ?N. ?N math:equalTo ?M. ?L rdf:first ?T; rdf:rest rdf:nil. ?T owl:onProperty ?P; owl:cardinality ?O. ?O math:equalTo ?M} => {?I owl:intersectionOf ?L}. {:owl14i3. ?L :item ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?L :item ?S. ?S owl:onProperty ?P; owl:minCardinality ?N. ?N math:equalTo ?M. ?C owl:onProperty ?P; owl:cardinality ?O. ?O math:equalTo ?M} => {?C owl:intersectionOf ?L}. {:owl15o1. ?U has owl:unionOf ?L. ?K :unions ?L} => {?U owl:oneOf ?K}. {:owl16c1. ?C has owl:complementOf ?R. ?R owl:onProperty ?P; owl:minCardinality ?N. (?N 1) math:difference ?M} => {?C owl:onProperty ?P; owl:maxCardinality ?M}. {:owl16c2. ?C has owl:complementOf ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. (?M 1) math:sum ?N} => {?C owl:onProperty ?P; owl:minCardinality ?N}. {:owl19p1. ?R owl:onProperty ?P; owl:minCardinality ?M. ?M math:equalTo 1. ?P has rdfs:range ?A. ?A has owl:oneOf ?L. ?L :item ?O. ?P has rdfs:range ?B. ?B has owl:oneOf ?K. ?K :item ?O. ?S a ?R} => {?S ?P ?O}. {:owl19p2. ?R owl:onProperty ?P; owl:someValuesFrom ?C. ?A has rdfs:subClassOf ?R. ?S a ?A} => {?S ?P _:O. _:O a ?C}. {:owl19d1. ?R owl:onProperty ?P; owl:cardinality ?M. ?P rdfs:range xsd:byte, xsd:unsignedInt. ?M math:notLessThan 128. ?N math:lessThan ?M. ?S a ?R} => {?S ?P ?N}. {:owl19d2. ?R owl:onProperty ?P; owl:someValuesFrom xsd:nonPositiveInteger. ?P rdfs:range xsd:nonNegativeInteger. ?N math:equalTo 0. ?S a ?R} => {?S ?P ?N}. ### inconsistency detections @@ {:owl20i2. ?A owl:equivalentClass owl:Nothing. ?X a ?A} => {{?A owl:equivalentClass owl:Nothing. ?X a ?A} log:inconsistentWith owl:}. {:owl20n1. rdf:nil rdf:first ?X} => {{rdf:nil rdf:first ?X} log:inconsistentWith owl:}. {:owl20n2. rdf:nil rdf:rest ?X} => {{rdf:nil rdf:rest ?X} log:inconsistentWith owl:}. {:owl20d1. ?Y owl:disjointWith ?Z. ?X a ?Y, ?Z} => {{?Y owl:disjointWith ?Z. ?X a ?Y, ?Z} log:inconsistentWith owl:}. {:owl20d0. ?Y owl:disjointWith ?X; owl:equivalentClass ?X} => {{?Y owl:disjointWith ?X; owl:equivalentClass ?X} log:inconsistentWith owl:}. {:owl20u1. ?P a owl:FunctionalProperty. ?S ?P ?X, ?Y. ?X owl:differentFrom ?Y} => {{?P a owl:FunctionalProperty. ?S ?P ?X, ?Y. ?X owl:differentFrom ?Y} log:inconsistentWith owl:}. {:owl20a1. ?P a owl:InverseFunctionalProperty. ?X ?P ?O. ?Y ?P ?O. ?X owl:differentFrom ?Y} => {{?P a owl:InverseFunctionalProperty. ?X ?P ?O. ?Y ?P ?O. ?X owl:differentFrom ?Y} log:inconsistentWith owl:}. {:owl20r0. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0. ?X ?P ?Y; a ?R} => {{?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0. ?X ?P ?Y; a ?R} log:inconsistentWith owl:}. {:owl20r1. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?X ?P ?Y1, ?Y2; a ?R. ?Y2 owl:differentFrom ?Y1} => {{?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?X ?P ?Y1, ?Y2; a ?R. ?Y2 owl:differentFrom ?Y1} log:inconsistentWith owl:}. {:owl20r2. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 2. ?X ?P ?Y1, ?Y2, ?Y3; a ?R. ?Y2 owl:differentFrom ?Y1. ?Y3 owl:differentFrom ?Y1, ?Y2} => {{?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 2. ?X ?P ?Y1, ?Y2, ?Y3; a ?R. ?Y2 owl:differentFrom ?Y1. ?Y3 owl:differentFrom ?Y1, ?Y2} log:inconsistentWith owl:}. {:owl21r1. ?R owl:onProperty ?P; owl:minCardinality ?M. ?P has rdfs:range ?X. ?X has owl:oneOf ?L. ?L :memberCount ?N. ?M math:greaterThan ?N} => {{?R owl:onProperty ?P; owl:minCardinality ?M. ?P has rdfs:range ?X. ?X has owl:oneOf ?L. ?L :memberCount ?N. ?M math:greaterThan ?N} log:inconsistentWith owl:}. {:owl20v2. ?R owl:onProperty ?P; owl:hasValue ?V. ?X ?P ?Y; a ?R. ?V owl:differentFrom ?Y} => {{?R owl:onProperty ?P; owl:hasValue ?V. ?X ?P ?Y; a ?R. ?V owl:differentFrom ?Y} log:inconsistentWith owl:}. {:owl20v3. ?R owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:equivalentClass owl:Nothing. ?X a ?R} => {{?R owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:equivalentClass owl:Nothing. ?X a ?R} log:inconsistentWith owl:}. {:owl20o0. ?C has owl:oneOf ?L. ?P rdfs:domain ?C. ?X ?P ?O. ?L :notItem ?X} => {{?C has owl:oneOf ?L. ?P rdfs:domain ?C. ?X ?P ?O. ?L :notItem ?X} log:inconsistentWith owl:}. {:owl20o1. ?C has owl:oneOf ?L. ?P rdfs:range ?C. ?S ?P ?X. ?L :notItem ?X} => {{?C has owl:oneOf ?L. ?P rdfs:range ?C. ?S ?P ?X. ?L :notItem ?X} log:inconsistentWith owl:}. {:owl20o2. ?C has owl:oneOf ?L. ?X a ?C. ?L :notItem ?X} => {{?C has owl:oneOf ?L. ?X a ?C. ?L :notItem ?X} log:inconsistentWith owl:}. {:owl30x1. ?P has rdf:type owl:FunctionalProperty. ?X ?P ?A^^rdf:XMLLiteral, ?B^^rdf:XMLLiteral. ?A log:notEqualTo ?B} => {{?P has rdf:type owl:FunctionalProperty. ?X ?P ?A^^rdf:XMLLiteral, ?B^^rdf:XMLLiteral. ?A log:notEqualTo ?B} log:inconsistentWith owl:}. {:owl30b1. ?R owl:onProperty ?P; owl:cardinality ?M. ?P rdfs:range xsd:byte. ?M math:greaterThan 256} => {{?R owl:onProperty ?P; owl:cardinality ?M. ?P rdfs:range xsd:byte. ?M math:greaterThan 256} log:inconsistentWith owl:}. {:owl30b2. ?R owl:onProperty ?P; owl:cardinality ?M. ?P rdfs:range xsd:byte, xsd:unsignedInt. ?M math:greaterThan 128} => {{?R owl:onProperty ?P; owl:cardinality ?M. ?P rdfs:range xsd:byte, xsd:unsignedInt. ?M math:greaterThan 128} log:inconsistentWith owl:}. ### support @@ {:owl40i1. ?S rdf:first ?X} => {?S :item ?X}. {:owl40i2. ?S rdf:rest ?B. ?B :item ?X} => {?S :item ?X}. {:owl40n1. ?X = ?X} => {rdf:nil :notItem ?X}. {:owl40n2. ?S rdf:first ?A. ?A owl:differentFrom ?X. ?S rdf:rest ?B. ?B :notItem ?X} => {?S :notItem ?X}. {:owl41i1. ?X = ?X} => {?X :includes rdf:nil}. {:owl41i2. ?S rdf:first ?A. ?X :item ?A. ?S rdf:rest ?B. ?X :includes ?B} => {?X :includes ?S}. {:owl42a1. ?X = ?X} => {?X :inAllOf rdf:nil}. {:owl42a2. ?S rdf:first ?A. ?X a ?A. ?S rdf:rest ?B. ?X :inAllOf ?B} => {?X :inAllOf ?S}. {:owl42s1. ?S rdf:first ?A. ?X a ?A} => {?X :inSomeOf ?S}. {:owl42s2. ?S rdf:rest ?B. ?X :inSomeOf ?B} => {?X :inSomeOf ?S}. {:owl43m1} => {rdf:nil :memberCount 0}. {:owl43m2. ?A rdf:rest ?B. ?B :memberCount ?M. (?M 1) math:sum ?N} => {?A :memberCount ?N}. {:owl44a1. ?C = ?C} => {rdf:nil :allClasses ?C}. {:owl44a2. ?L rdf:first ?A; rdf:rest ?B. ?A owl:equivalentClass ?C. ?B :allClasses ?C} => {?L :allClasses ?C}. {:owl44s1. ?L rdf:first ?A. ?A owl:equivalentClass ?C} => {?L :someClasses ?C}. {:owl44s2. ?L rdf:rest ?B. ?B :someClasses ?C} => {?L :someClasses ?C}. {:owl45r1. ?P = ?P} => {?P :reflexive rdf:nil}. {:owl45r2. ?S rdf:first ?A. ?A ?P ?A. ?S rdf:rest ?B. ?P :reflexive ?B} => {?P :reflexive ?S}. {:owl50o1. ?L rdf:first ?O. ?O has owl:oneOf ?J. ?J :item ?A} => {?L :oneItem ?A}. {:owl50o2. ?L rdf:rest ?B. ?B :oneItem ?A} => {?L :oneItem ?A}. {:owl51o1. ?L = ?L} => {?L :ones rdf:nil}. {:owl51o2. ?K rdf:first ?A. ?L :oneItem ?A. ?K rdf:rest ?B. ?L :ones ?B} => {?L :ones ?K}. {:owl51u1. ?K = ?K} => {?K :unions rdf:nil}. {:owl51u2. ?L rdf:first ?O. ?O has owl:oneOf ?J. ?J :item ?A. ?K :item ?A. ?L rdf:rest ?B. ?K :unions ?B} => {?K :unions ?L}. {:owl53o1. ?R owl:someValuesFrom ?C} => {?R :someOrAll ?C}. {:owl53o2. ?R owl:allValuesFrom ?C} => {?R :someOrAll ?C}.