Forall ?p ?o ?s (
    ?s[owl:sameAs->?s] :- ?s[?p->?o] )

Forall ?p ?o ?s (
    ?p[owl:sameAs->?p] :- ?s[?p->?o] )

Forall ?p ?o ?s (
    ?o[owl:sameAs->?o] :- ?s[?p->?o] )

Forall ?x ?y (
    ?y[owl:sameAs->?x] :- ?x[owl:sameAs->?y] )

Forall ?x ?z ?y (
    ?x[owl:sameAs->?z] :- And(
        ?x[owl:sameAs->?y]
        ?y[owl:sameAs->?z]  ))

Forall ?p ?o ?s ?sp (
    ?sp[?p->?o] :- And(
        ?s[owl:sameAs->?sp]
        ?s[?p->?o]  ))

Forall ?p ?o ?pp ?s (
    ?s[?pp->?o] :- And(
        ?p[owl:sameAs->?pp]
        ?s[?p->?o]  ))

Forall ?p ?o ?s ?op (
    ?s[?p->?op] :- And(
        ?o[owl:sameAs->?op]
        ?s[?p->?o]  ))

Forall ?x ?y (
    rif:error("inconsistent") :- And(
        ?x[owl:sameAs->?y]
        ?x[owl:differentFrom->?y]  ))

Forall ?p ?c ?x ?y (
    ?x[rdf:type->?c] :- And(
        ?p[rdfs:domain->?c]
        ?x[?p->?y]  ))

Forall ?p ?c ?x ?y (
    ?y[rdf:type->?c] :- And(
        ?p[rdfs:range->?c]
        ?x[?p->?y]  ))

Forall ?p ?y2 ?x ?y1 (
    ?y1[owl:sameAs->?y2] :- And(
        ?p[rdf:type->owl:FunctionalProperty]
        ?x[?p->?y1]
        ?x[?p->?y2]  ))

Forall ?p ?x1 ?x2 ?y (
    ?x1[owl:sameAs->?x2] :- And(
        ?p[rdf:type->owl:InverseFunctionalProperty]
        ?x1[?p->?y]
        ?x2[?p->?y]  ))

Forall ?p ?x ?z ?y (
    ?x[?p->?x] :- And(
        ?p[rdf:type->owl:ReflexiveProperty]
        ?x[?y->?z]  ))

Forall ?p ?x ?z ?y (
    ?y[?p->?y] :- And(
        ?p[rdf:type->owl:ReflexiveProperty]
        ?x[?y->?z]  ))

Forall ?p ?x ?z ?y (
    ?z[?p->?z] :- And(
        ?p[rdf:type->owl:ReflexiveProperty]
        ?x[?y->?z]  ))

Forall ?p ?x (
    rif:error("inconsistent") :- And(
        ?p[rdf:type->owl:IrreflexiveProperty]
        ?x[?p->?x]  ))

Forall ?p ?x ?y (
    ?y[?p->?x] :- And(
        ?p[rdf:type->owl:SymmetricProperty]
        ?x[?p->?y]  ))

Forall ?p ?x ?y (
    rif:error("inconsistent") :- And(
        ?p[rdf:type->owl:AsymmetricProperty]
        ?x[?p->?y]
        ?y[?p->?x]  ))

Forall ?p ?x ?z ?y (
    ?x[?p->?z] :- And(
        ?p[rdf:type->owl:TransitiveProperty]
        ?x[?p->?y]
        ?y[?p->?z]  ))

Forall ?x ?y ?p2 ?p1 (
    ?x[?p2->?y] :- And(
        ?p1[rdfs:subPropertyOf->?p2]
        ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
    ?x[?p2->?y] :- And(
        ?p1[owl:equivalentProperty->?p2]
        ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
    ?x[?p1->?y] :- And(
        ?p1[owl:equivalentProperty->?p2]
        ?x[?p2->?y]  ))

Forall ?x ?y ?p2 ?p1 (
    rif:error("inconsistent") :- And(
        ?p1[owl:propertyDisjointWith->?p2]
        ?x[?p1->?y]
        ?x[?p2->?y]  ))

Forall ?x ?y ?p2 ?p1 (
    ?y[?p2->?x] :- And(
        ?p1[owl:inverseOf->?p2]
        ?x[?p1->?y]  ))

Forall ?x ?y ?p2 ?p1 (
    ?y[?p1->?x] :- And(
        ?p1[owl:inverseOf->?p2]
        ?x[?p2->?y]  ))

Forall ?p ?v ?u ?x ?y (
    ?u[rdf:type->?x] :- And(
        ?x[owl:someValuesFrom->?y]
        ?x[owl:onProperty->?p]
        ?u[?p->?v]
        ?v[rdf:type->?y]  ))

Forall ?p ?v ?u ?x ?y (
    ?v[rdf:type->?y] :- And(
        ?x[owl:allValuesFrom->?y]
        ?x[owl:onProperty->?p]
        ?u[rdf:type->?x]
        ?u[?p->?v]  ))

Forall ?p ?u ?x ?y (
    ?u[?p->?y] :- And(
        ?x[owl:hasValue->?y]
        ?x[owl:onProperty->?p]
        ?u[rdf:type->?x]  ))

Forall ?p ?u ?x ?y (
    ?u[rdf:type->?x] :- And(
        ?x[owl:hasValue->?y]
        ?x[owl:onProperty->?p]
        ?u[?p->?y]  ))

Forall ?p ?u ?x ?y (
    rif:error("inconsistent") :- And(
        ?x[owl:maxCardinality->0]
        ?x[owl:onProperty->?p]
        ?u[?p->?y]
        ?u[rdf:type->?x]  ))

Forall ?p ?y2 ?u ?x ?y1 (
    ?y1[owl:sameAs->?y2] :- And(
        ?x[owl:maxCardinality->1]
        ?x[owl:onProperty->?p]
        ?u[?p->?y1]
        ?u[?p->?y2]
        ?u[rdf:type->?x]  ))

Forall ?x ?c1 ?c2 (
    ?x[rdf:type->?c2] :- And(
        ?c1[rdfs:subClassOf->?c2]
        ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
    ?x[rdf:type->?c2] :- And(
        ?c1[owl:equivalentClass->?c2]
        ?x[rdf:type->?c1]  ))

Forall ?x ?c1 ?c2 (
    ?x[rdf:type->?c1] :- And(
        ?c1[owl:equivalentClass->?c2]
        ?x[rdf:type->?c2]  ))

Forall ?x ?c1 ?c2 (
    rif:error("inconsistent") :- And(
        ?c1[owl:disjointWith->?c2]
        ?x[rdf:type->?c1]
        ?x[rdf:type->?c2]  ))

Forall ?c (
    ?c[rdfs:subClassOf->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c (
    ?c[owl:equivalentClass->?c] :- ?c[rdf:type->owl:Class] )

Forall ?c1 ?c2 ?c3 (
    ?c1[rdfs:subClassOf->?c3] :- And(
        ?c1[rdfs:subClassOf->?c2]
        ?c2[rdfs:subClassOf->?c3]  ))

Forall ?c1 ?c2 (
    ?c1[rdfs:subClassOf->?c2] :- ?c1[owl:equivalentClass->?c2] )

Forall ?c1 ?c2 (
    ?c2[rdfs:subClassOf->?c1] :- ?c1[owl:equivalentClass->?c2] )

Forall ?p (
    ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
    ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:ObjectProperty] )

Forall ?p (
    ?p[rdfs:subPropertyOf->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p (
    ?p[owl:equivalentProperty->?p] :- ?p[rdf:type->owl:DatatypeProperty] )

Forall ?p3 ?p2 ?p1 (
    ?p1[rdfs:subPropertyOf->?p3] :- And(
        ?p1[rdfs:subPropertyOf->?p2]
        ?p2[rdfs:subPropertyOf->?p3]  ))

Forall ?p2 ?p1 (
    ?p1[rdfs:subPropertyOf->?p2] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p2 ?p1 (
    ?p2[rdfs:subPropertyOf->?p1] :- ?p1[owl:equivalentProperty->?p2] )

Forall ?p ?c1 ?c2 (
    ?p[rdfs:domain->?c2] :- And(
        ?p[rdfs:domain->?c1]
        ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
    ?p1[rdfs:domain->?c] :- And(
        ?p2[rdfs:domain->?c]
        ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?c1 ?c2 (
    ?p[rdfs:range->?c2] :- And(
        ?p[rdfs:range->?c1]
        ?c1[rdfs:subClassOf->?c2]  ))

Forall ?c ?p2 ?p1 (
    ?p1[rdfs:range->?c] :- And(
        ?p2[rdfs:range->?c]
        ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?c1 ?c2 ?i ?p2 ?p1 (
    ?c1[rdfs:subClassOf->?c2] :- And(
        ?c1[owl:hasValue->?i]
        ?c1[owl:onProperty->?p1]
        ?c2[owl:hasValue->?i]
        ?c2[owl:onProperty->?p2]
        ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?y2 ?c1 ?c2 ?y1 (
    ?c1[rdfs:subClassOf->?c2] :- And(
        ?c1[owl:someValuesFrom->?y1]
        ?c1[owl:onProperty->?p]
        ?c2[owl:someValuesFrom->?y2]
        ?c2[owl:onProperty->?p]
        ?y1[rdfs:subClassOf->?y2]  ))

Forall ?c1 ?c2 ?y ?p2 ?p1 (
    ?c1[rdfs:subClassOf->?c2] :- And(
        ?c1[owl:someValuesFrom->?y]
        ?c1[owl:onProperty->?p1]
        ?c2[owl:someValuesFrom->?y]
        ?c2[owl:onProperty->?p2]
        ?p1[rdfs:subPropertyOf->?p2]  ))

Forall ?p ?y2 ?c1 ?c2 ?y1 (
    ?c1[rdfs:subClassOf->?c2] :- And(
        ?c1[owl:allValuesFrom->?y1]
        ?c1[owl:onProperty->?p]
        ?c2[owl:allValuesFrom->?y2]
        ?c2[owl:onProperty->?p]
        ?y1[rdfs:subClassOf->?y2]  ))

Forall ?c1 ?c2 ?y ?p2 ?p1 (
    ?c2[rdfs:subClassOf->?c1] :- And(
        ?c1[owl:allValuesFrom->?y]
        ?c1[owl:onProperty->?p1]
        ?c2[owl:allValuesFrom->?y]
        ?c2[owl:onProperty->?p2]
        ?p1[rdfs:subPropertyOf->?p2]  ))