true => p(a).
p(X) => p(f(X)) ; q(X).
p(f(a)) => goal.
q(X) => goal.