Trace the use of linear-input resolution to find a refutation of each of the following clause sets. Use the "Prolog style" execution rules, i.e., using a negative top clause, selecting the left most literal, search for a resolution partner top-down, and adding side clause literals to the left. Mark backtracking points with a *. For the second set, things get weird. Explain what you might do to fix the "weirdness", and explain why you might be surprised that linear-input resolution works even then.
{ ~r(Y) | ~p(Y),
p(b),
r(a),
p(S) | ~p(b) | ~r(S),
r(c) }
{ p(X) | ~p(f(X))
~p(a)
p(S) | q(S) | r(S)
~q(T) | p(a)
~r(T) | p(a) }