Oh I see its from “Metacircular Interpreter (Prolog)” in your notes.
In these notes, some propositonal provers are burried:
Computational Logic Notes
How about a prover that can also do FOL? Do I need to combine
skolemization with something? But resolution says propositional only?
P.S.: Its an open challenge here Terminology: "true", "entailed", "provable", "holds" - #15 .
Here Schubert's Steamroller in Prolog - #5 by bwat something was first negation as failure,
but then Eco Logic came into play, the later I didn’t understand.