I found a problem which is a definite program problem and ask to obtain all SDLNF derivations of the generic goal.
$Product(x,y) ← Quantity(x),Rate(y)$
$Rate(x) ← Sub(x)$
$Quantity(a)$
$Quantity(b)$
$Quantity(f(a))$
$Rate(f(a))$
$Rate(f(b))$
$Sub(f(f(a)))$
(There ain't no meaning of what names imply. I just used some words for P,Q,R,S)
and the General goal is $← Product(x,f(x)),¬Quantity(f(x))$
So I started to solve this.This is how I started,
$G0$ : $← Product(x,f(x)),¬Quantity(f(x))$
$C0$ : $Product(x,y) ← Quantity(x),Rate(y)$
$G1$ : $← Quantity(x),Rate(f(x)),¬Quantity(f(x))$
$C1$ : $ Quantity(a)$
$G2$ : $← Rate(f(a)),¬Quantity(f(a))$
$C2$ : $ Rate(f(a))$ -- Here it is not unifiable to remove $ Rate(f(a))$ and obtain $G3$ . I mean if it was something like $ Rate(f(d))$ then I can remove it by using Rate(f(a)) and unifier($σ$) for that would be $ σ={d/a} $. But here $ σ={a/a} $ which is according to the theory is not unifiable.
So For me this seems like does not have a SDLNF refutation. Am I missing something? Does this have a refutation?