Careful with the resolution theorem prover

Help!
1

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),

https://www.metalevel.at/logic/plres.pl

Mentioned here:

Theorem Proving with Prolog
https://www.metalevel.at/prolog/theoremproving

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?