Improving Beckert's & Posegga's in Prolog

Joseph Vidal Rosset expressed some regret that his Prolog capabilities are limited. Maybe we can pool on others Prolog programming capabilities. So here is the callenge, provide Beckert & Posegga in Prolog.

Beckert & Posegga is usually pitched as being the shortest first order logic prover around. But there is a catch, namely it needs a preparation step, the formula needs to be braught in a special form before it can be tried by the prover.

So in the end the prover will not only be the epic few lines from here, but a little more:

Anybody up to the challenge, including running the Pelletier’s problems.
And how about display found proofs?

Edit 10.09.2020:
Cross posted on Stackoverflow: