Careful with the resolution theorem prover

One finds readily the following resolution theorem prover on the internet,
it now says it runs with Scryer Prolog, but my suspicion is that it also
runs with SWI-Prolog, or did run with SWI-Prolog in the past:

Resolution Calculus for Propositional Logic

pl_resolvent( ... ) :-
         select(Q, As0, As),
         select(not(Q), Bs0, Bs),
         append(As, Bs, Rs0),

Mentioned here:

Theorem Proving with Prolog

But when one reads the fine print by Markus Triska, it says for propositional logic.
Not sure whether it works for first order logic (FOL) as well? There is a FOL
example {p(X), p(Y)} and {~p(U), ~p(V)} which hints that a full flegded resolution

theorem prover needs also “factoring”. Making a resolution theorem prover
only complete when it implements resolution step with factoring:

where τ is a variable renaming on Φ
where Φ’ is a factor of Φτ and φ∈Φ’
where Ψ’ is a factor of Ψ and ¬ψ∈Ψ’
where σ=mgu(φ, ψ)
Introduction to Logic - Chapter 14

Any full fledged resolution theorem provers around written in
Prolog that can be run for example with the SWI-Prolog system?