Here is the SWI-Prolog code of Fitting’s leanTap revisited:

:- use_module(library(lists)).
:- use_module(library(statistics)).

% :- use_module(library(dom)).
% operator definitions (TPTP syntax)

:- op( 500, fy, ~).             % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional

/*
Next, a classification of formula types,
& instances.
*/

type(X & Y, conj, X, Y).
type(~(X & Y), disj, ~ X, ~ Y).
type(X | Y, disj, X, Y).
type(~(X | Y), conj, ~ X, ~ Y).
type(X => Y, disj, ~ X, Y).
type(~(X => Y), conj, X, ~ Y).
type(X <=> Y, disj, X & Y, ~ X & ~ Y).
type(~(X <=> Y), disj, X & ~ Y, ~ X & Y).
type(~ (~ (X)), doub, X, _).
/*
Now the heart of the matter.
thm(Lambda, Gamma) :-
the sequent Lambda --> Gamma is provable.
*/

thm(Lambda, [Doubleneg | Gamma]) :- 
        type(Doubleneg, doub, X, _), !,
        thm(Lambda, [X | Gamma]).

thm(Lambda, [Beta | Gamma]) :-
        type(Beta, disj, Beta1, Beta2), !,
        thm(Lambda, [Beta1, Beta2 | Gamma]).

thm(Lambda, [Alpha | Gamma]) :-
        type(Alpha, conj, Alpha1, Alpha2), !,
        thm(Lambda, [Alpha1 | Gamma]), !,
        thm(Lambda, [Alpha2 | Gamma]).

thm([L1|Lambda], [L2|_]) :-
        (
          L1 = L2, !
        ;
          thm(Lambda, [L2])
        ).

thm(Lambda, [~ L | Gamma]) :-
        thm([L | Lambda], Gamma), !.

thm(Lambda, [L | Gamma]) :-
        thm([~ L | Lambda], Gamma), !.
/*
Finally, the driver.
*/
prove(X) :-
time(thm([], [X])).

This code according to Fitting provides a sequent calculus. I have tried to change minimally this code to get a Prolog Print of each proof, with input prove(X, Proof), following the structure of Jen Otten’s prover (online here
and here):

% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------
:- use_module(library(lists)).

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % implication

% -----------------------------------------------------------------
provable(F, P) :- time(prove([] > [F], P)).
% -----------------------------------------------------------------

% axiom
prove(G > D, ax(G > D, A)) :- member(A,G), member(B,D), A == B, !.

% conjunction
prove(G > D, land(G > D, P) ) :- select1( (A & B) ,G,G1), !,
                prove([A , B | G1] > D, P).

prove(G > D, rand(G > D, P1,P2)) :- select1( (A & B) ,D,D1), !,
                prove(G > [A|D1], P1), prove(G > [B|D1], P2).

% disjunction
prove(G > D, lor(G > D, P1,P2)) :- select1((A | B),G,G1), !,
                prove([A|G1] > D, P1), prove([B|G1] > D, P2).

prove(G > D, ror(G > D, P)) :- select1( (A | B),D,D1), !,
                prove(G > [A,B|D1], P ).

% implication
prove(G > D, limpl(G > D, P1,P2)) :- select1((A => B),G,G1), !,
                prove(G1 > [A|D], P1), prove([B|G1] > D, P2).

prove(G > D, rimpl(G > D, P)) :- select1((A => B),D,D1), !,
                prove([A|G] > [B|D1], P).

% negation
prove(G > D, lneg(G > D, P)) :- select1( ~A,G,G1), !,
                prove(G1 > [A|D], P).

prove(G > D, rneg(G > D, P)) :- select1(~A ,D,D1), !,
                prove([A|G] > D1, P).

% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------

For example :

• provable((p => p), Proof).
  % 22 inferences, 0.000 CPU in 0.000 seconds (95% CPU, 1132503 Lips)
  Proof = rimpl([]>[(p=>p)], ax([p]>[p], p))

But all my tentatives to get from Fitting’s prover (that is complete) a prover that provides a proof like P above have failed. Any help that could put me on the right road is welcome.