TBox:
01	EXISTS R ISA  A
02	EXISTS R- ISA B
03	EXISTS Q ISA A
04	EXISTS Q- ISA C
05	A ISA EXISTS Q
06	FUNC Q
07	Q ISA R
08	C ISA A
09	C ISA B
10	D ISA B
11	C ISA NOT D
ABox:
Q(a,b)
R(b,b)
C(c)

Query: 
q(x) :- R(x,y),R(y,z),A(z)

Espansioni (solo alcune)

Prima espansione:
q(x) :- R(x,y),R(y,z),A(z)
q(x) :- R(x,y),R(y,z),C(z)   -- rewrite con 08
q(x) :- R(x,y),R(y,z),Q(_, z)   -- rewrite con 04
q(x) :- Q(x,y),R(y,z),Q(_, z)   -- rewrite con 07
q(x) :- Q(x,y),Q(y,z),Q(_, z)   -- rewrite con 07
q(x) :- Q(x,y),Q(y,z)   -- unify Q(y,z) = Q(_,z)
q(x) :- Q(x,y),A(y)   -- rewrite 05
q(x) :- Q(x,y),C(y)   -- rewrite 08
q(x) :- Q(x,y),Q(_,y)   -- rewrite 04
q(x) :- Q(x,y)   -- unify Q(x,y) = Q(_,z)
---> dall’asserzione ABox Q(a,b)  si ottiene la risposta a 
q(x) :- A(x)  -- rewrite 05
q(x) :- C(x)   -- rewrite 08
---> dall’asserzione ABox C(c)  si ottiene la risposta c 

Seconda espansione:
q(x) :- R(x,y),R(y,z),A(z)
q(x) :- R(x,y),R(y,z),R(z,_)  -- rewrite 01
q(x) :- R(x,y),R(z,z)  -- unify R(y,z) = R(z,_) 
q(x) :- R(x,x)  -- unify R(x,y) = R(z,z) 
---> dall’asserzione ABox R(b,b)  si ottiene la risposta b