Is there a way to infer existentially quantified statements in OWL?

Question

Consider the following chain of reasoning:

 1. Simba is a lion.
 2. All lions have at least one parent.
 3. So, Simba has at least one parent.

This is a perfectly valid inference, and it can be represented in predicate logic as follows:

s = Simba
L = is a lion
P = is the parent of

1. Ls
2. (Ax)(Lx --> (Ey)(Pxy))
3. (Ey)(Pys)

In a natural deduction system, one would be permitted to infer 3 (via a series of inference rules) from the conjunction of 1 and 2.

I would expect to see a similar inference generated with OWL reasoners. Suppose we had the following triples (using Turtle syntax):

:Simba rdf:type :Lion .

:Lion a owl:Class ;
   rdfs:subClassOf
   [
      a owl:Restriction ;
      owl:onProperty :isParentOf ;
      owl:someValuesFrom owl:Thing ;
   ] ;
   .

These statements are translations of 1 and 2 into OWL. However, it appears that OWL reasoners do not infer something like 3. Is this right? Or can something like this inference be made using OWL reasoners?