Contradicting axioms for reflexive object property

[b-gehrke]

The translation of the OWL ReflexiveObjectProperty(R) axiom to the FOL ![X0]:'R'(X0,X0) axiom contradicts the following object property and background axioms

% background axiom: object domain and data domain are disjoint
![X]:('thing'(X)=>~'literal'(X)))
% background axiom: there are literals
?[X]:'literal'(X)

% Declaration(ObjectProperty(<http://example.com/R>))
![X,Y]:('R'(X,Y)=>'thing'(X))

Consider this simple ontology in Manchester Syntax:

Prefix: : <http://example.com/>

Ontology:

ObjectProperty: R
  Characteristics: Reflexive

The translated FOL theory is inconsistent. EProver outputs

#cnf(i_0_3, plain, ('thing'(esk1_0))).
#
#cnf(i_0_4, plain, ('literal'(esk2_0))).
#
#cnf(i_0_29, plain, ('R'(X1,X1))).
#
#cnf(i_0_2, plain, (~'literal'(X1)|~'thing'(X1))).
#
#cnf(i_0_1, plain, ('literal'(X1)|'thing'(X1))).
#
#cnf(i_0_28, plain, ('thing'(X2)|~'R'(X1,X2))).
#
#cnf(i_0_33, plain, ('thing'(X1))).
#
#cnf(i_0_2, plain, (~'literal'(X1))).
# Proof found!
# SZS status ContradictoryAxioms

[sfluegel05]

This is indeed a problem in the specification: For reflexive object properties, it states that $\forall x: R(x, x)$. Instead, it should say: $\forall x: (owl:Thing(x) \rightarrow R(x,x))$.