How to reverse the output of proof printing in this fork of seqprover.pl

Hello everybody,
Below seqprover.pl, the FOL prover written by Naoyuki Tamura. I have added a section to get LaTeX proofs for bussproofs.sty (the original code gives proofs for proof.sty). That works almost perfectly: proofs are exactly in the reverse order and I do not succeed at all to use reverse/2 correctly to get the expected result. Here is the code (tex section has been deleted for the message):

%%%
%%%  Sequent Calculus Prover in Prolog
%%%  by Naoyuki Tamura (tamura@kobe-u.ac.jp)
%%%  TeX form output by Eiji Sugiyama
%%%
%%%  You can freely distribute or modify this program.
%%%
%%%  Version 2.0
%%%    12/30/2020 Modified for SWI Prolog
%%%
:- dynamic
	seq_system/2, threshold/1, output_form/1, logging/2,
	output_count/1, output_result/2,
	proved/3, not_proved/2, axiom/1.
%seq_system(cl,first).
%threshold(5).
%output_form(pretty).
%logging(no, _).
%output_count(1).

:- op(1200, xfx, [ -->, <--> ]).
:- op( 900, xfy, [ -> ]).
% :- op( 850, xfy, [ -> ]).
:- op( 850, xfy, [ /\, \/ ]).
:- op( 800, fy,  [ ~ ]).
:- op( 750, xfy, [ @, # ]).

prover :-
	writex('Sequent Calculus Prover ver 2.0 in Prolog'), nlx,
	writex('        by Naoyuki Tamura (tamura@kobe-u.ac.jp)'), nlx,
%	seq_init,
	statistics(runtime, [T0,_]),
	seq_prover,
	statistics(runtime, [T1,_]),
	T is T1-T0,
	writex('Exit from Sequent Calculus Prover...'), nlx,
	writex('Total CPU time = '), writex(T), writex(' msec.'), nlx,
	log_end.

seq_init :-
	set_system(cl,first),
	set_threshold(5),
	set_axioms([]),
	set_output_form(pretty),
	log_end,
	reset_output_result.

seq_prover :-
	current_input(STR),
	seq_prover(STR).

seq_prover(STR) :-
        prompt(_, ''),
	repeat,
	  seq_system(Sys, Opt),
	  writex(Sys), writex('('), writex(Opt), writex(')'),
	  writex('> '),
          flush_out,
	  readx(STR, X),
	  seq_command(X),
	seq_quit(X),
	close(STR).

seq_quit(X) :-
	nonvar(X),
	memberq(X, [quit, end, bye, halt, end_of_file]).

seq_command(X) :-
	seq_execute(X),
	!,
	writex(yes), nlx.
seq_command(_) :-
	writex(no), nlx.

seq_execute(X) :- var(X), !, fail.
seq_execute(X) :- seq_quit(X), !.
seq_execute(help) :- !, seq_help.
seq_execute(init) :- !, seq_init.
seq_execute([File]) :- !, seq_consult(File).
seq_execute(cl(Opt)) :- !, set_system(cl,Opt).
%seq_execute(il(Opt)) :- !, set_system(il,Opt).
seq_execute(threshold(N)) :- var(N), !,
	threshold(N),
	writex(threshold(N)), nlx.
seq_execute(threshold(N)) :- !,
	set_threshold(N).
seq_execute(axioms(As)) :- var(As), !,
	(bagof(A, axiom(([]-->[A])), As); As=[]), !,
	writex(axioms(As)), nlx.
seq_execute(axioms(As)) :- !,
	set_axioms(As).
seq_execute(output(Form)) :- var(Form), !,
	output_form(Form),
	writex(output(Form)), nlx.
seq_execute(output(Form)) :-
	set_output_form(Form).
seq_execute(log(File)) :- var(File), !,
	logging(File, _),
	writex(log(File)), nlx.
seq_execute(log(no)) :- !,
	log_end.
seq_execute(log(File)) :- !,
	log_start(File).
seq_execute(N) :- integer(N), !,
	get_output_result(N, N1, P),
	print_output(N1, P).
seq_execute((Xs <--> Ys)) :- !,
	seq_execute((Xs --> Ys)),
	seq_execute((Ys --> Xs)).
seq_execute((Xs --> Ys)) :-
	convert_to_seq((Xs --> Ys), Seq),
	sequentq(Seq),
	!,
	seq_prove(Seq).
seq_execute(X) :-
	writex('Error '),
	writex(X),
	writex(' is not a command nor a sequent.'), nlx.

seq_help :-
	writex('A1,...,Am -->  B1,...,Bn : Try to prove the sequent.'), nlx,
	writex('A1,...,Am <--> B1,...,Bn : Try to prove the sequent '),
	    writex('in both directions.'), nlx,
	writex('help           : Help.'), nlx,
	writex('init           : Initialize the prover.'), nlx,
	writex('[File]         : Read from the file.'), nlx,
	writex('Sys(Opt)       : Select the system. '),
	    writex('Sys={cl}, Opt={first|prop}'), nlx,
	writex('threshold(N)   : Set/retrieve the threshold. N>=0'), nlx,
	writex('axioms(Axioms) : Set/retrieve the axioms. '), 
	    writex('Axioms=[A1,...,Am]'), nlx,
	writex('output(Form)   : Set/retrieve the output form. '), 
	    writex('Form={pretty|tex|standard|term}'), nlx,
	writex('log(L)         : Start/stop/retrieve the output logging. '), 
	    writex('L={yes|File|no}'), nlx,
	writex('N              : Display the N-th output.'), nlx,
	writex('quit           : Quit.'), nlx.

seq_consult(File) :-
	open(File, read, STR),
	seq_prover(STR).

seq_prove(Seq) :-
	statistics(runtime,[_,_]),
	prove(Seq, Proof),
	statistics(runtime,[_,Time]),
	writex('Succeed in proving '), 
	write_seq(Seq),
	writex(' ('), writex(Time), writex(' msec.)'), nlx,
	output_count(N),
	assert_output_result(Proof),
	!,
	print_output(N, Proof).
seq_prove(Seq) :-
	statistics(runtime,[_,Time]),
	writex('Fail to prove '),
	write_seq(Seq),
	writex(' ('), writex(Time), writex(' msec.)'), nlx.

print_output(N, P) :-
	output_form(Form), writex(Form), writex(':'),
	writex(N), writex(' ='), nlx,
	print_proof(P).

print_proof(P) :-
	output_form(Form),
	print_proof_form(Form, P).

print_proof_form(pretty, P) :- !,
	pretty_print(P).


print_proof_form(buss, P) :- !,
	buss_tex_print(P).

print_proof_form(standard, P) :- !,
	standard_print(P).
print_proof_form(term, P) :- !,
	writex(P), nlx.

set_system(Sys, Opt) :-
	memberq(Sys, [cl]),
	memberq(Opt, [prop,first]),
	retractall(seq_system(_,_)),
	assert(seq_system(Sys,Opt)).

set_threshold(N) :-
	integer(N), N >= 0,
	retractall(threshold(_)),
	assert(threshold(N)).

set_axioms(Axioms) :-
	retractall(axiom(_)),
	assert_axioms(Axioms).

assert_axioms([]).
assert_axioms([A|As]) :-
	formulaq(A),
	!,
	assert(axiom(([]-->[A]))),
	assert_axioms(As).
assert_axioms([A|As]) :-
	writex('Error '), writex(A),
	writex(' is not a formula.'), nlx,
	assert_axioms(As).

set_output_form(Form) :-
	memberq(Form, [pretty, tex, buss, standard, term]),
	retractall(output_form(_)),
	assert(output_form(Form)).

reset_output_result :-
	retractall(output_count(_)),
	retractall(output_result(_,_)),
	assert(output_count(1)).

assert_output_result(P) :-
	output_count(N),
	assert(output_result(N,P)),
	retractall(output_count(_)),
	N1 is N+1,
	assert(output_count(N1)).

get_output_result(N, N, P) :- N>0, !,
	output_result(N, P).
get_output_result(N, N1, P) :-
	output_count(M),
	N1 is M+N,
	output_result(N1, P).

convert_to_seq((Xs --> Ys), (Xs1 --> Ys1)) :-
	convert_to_list(Xs, Xs1), convert_to_list(Ys, Ys1).

convert_to_list(X, _) :- var(X), !, fail.
convert_to_list([], []) :- !.
convert_to_list([X|Xs], [X|Xs]) :- !.
convert_to_list((X,Xs), [X|Zs]) :- !, convert_to_list(Xs, Zs).
convert_to_list(X, [X]).

sequentq((X-->Y)) :- formula_listq(X), formula_listq(Y).

formula_listq([]).
formula_listq([A|As]) :- formulaq(A), formula_listq(As).

formulaq(A) :- var(A), !, fail.
formulaq((_-->_)) :- !, fail.
formulaq([]) :- !, fail.
formulaq([_|_]) :- !, fail.
formulaq(~A) :- !, formulaq(A).
formulaq(A/\B) :- !, formulaq(A), formulaq(B).
formulaq(A\/B) :- !, formulaq(A), formulaq(B).
formulaq(A->B) :- !, formulaq(A), formulaq(B).
formulaq(_X@A) :- !, formulaq(A).
formulaq(_X#A) :- !, formulaq(A).
formulaq(_).

%%
%%  Sequent Calculus Prover
%%
%%  seq_system( {cl}, {prop|first} ).
%%    seq_system(cl,first).
%%  Max number of cut and contraction rules: cut, r(all), l(exists)
%%    threshold(5).
%%  Axioms
%%    axiom(Ax1). axiom(Ax2). ....

prove(S, P) :-
	retractall(proved(_,_,_)),
	retractall(not_proved(_,_)),
	threshold(N),
	writex('Trying to prove with threshold ='),
	for(I, 0, N),
	writex(' '), writex(I),
	flush_out,
	prove(S, P, I),
	nlx,
	!.
prove(_S, _P) :-
	nlx,
	fail.

prove(S, _P, N) :-
	ground(S),
	clause(not_proved(S,M), _),
	N =< M,
	!,
	fail.
prove(S, P, N) :-
	ground(S),
	clause(proved(S,P,M), _),
	M =< N,
	!.
prove(S, P, _N) :-
	clause(axiom(S), _),
	P = [axiom,[[]],S],
	!.
prove(S, P, N) :-
	check_sequent(S),
	select_rule(Rule, S, Ss, Pos),
	P = [Rule,Pos,S|Ps],
	set_sequents(Ss, Ps),
	rule_constraint(Rule, Ps, M),
	N1 is N-M, N1 >= 0,
       	prove_all(Ss, Ps, N1),
%	!,
	assert(proved(S,P,N)).
prove(S, _P, N) :-
	ground(S),
	assert(not_proved(S,N)),
	!,
	fail.

prove_all([], [], _N).
prove_all([S|Ss], [P|Ps], N) :-
	prove(S, P, N),
	prove_all(Ss, Ps, N).

check_sequent((X-->Y)) :-
	length(X, N1), length(Y, N2),
	N1 + N2 < 20.
%check_sequent(_) :- seq_system(cl,_), !.
%check_sequent((_X-->Y)) :- (Y=[]; Y=[_]), !.

select_rule(Rule, S, Ss, Pos) :-
	rule(RuleSys, inv, Rule, S, Ss, Pos),
	check_rule(RuleSys),
	!.
select_rule(Rule, S, Ss, Pos) :-
	rule(RuleSys, no, Rule, S, Ss, Pos),
	check_rule(RuleSys).

check_rule([RSys,ROp]) :-
	seq_system(Sys, Op),
	check_rule1(Sys, RSys),
	check_rule2(Op, ROp),
	!.

check_rule1(Sys, Sys).
check_rule1(cl, _).

check_rule2(Op, Op).
check_rule2(first, _).

set_sequents([], []).
set_sequents([S|Ss], [[_,_,S|_]|Ps]) :- set_sequents(Ss, Ps).

rule_constraint(cut, [P1,_P2], 1) :- !,
	axiom(S1),
	P1 = [axiom,_,S1].
% bug report from Joseph Vidal-Rosset
rule_constraint(l(all), [P1], 1) :- !,
	P1 = [NextRule,_,_|_],
	dif(NextRule, l(all)).
rule_constraint(r(exists), [P1], 1) :- !,
	P1 = [NextRule,_,_|_],
	dif(NextRule, r(exists)).
rule_constraint(_Rule, _, 0).

% Logical axiom
% cannot be invertible owing to unification
rule([cl,prop], no, ax, S, [], [[]]) :-
	match(S,  ([_X1,[A],_X2]-->[_Y1,[A],_Y2])).
% Rules for the propositional constants
rule([cl,prop], inv, l(top), S, [S1], [l(N),[]]) :-
	match(S,  ([X1,[top],X2]-->[Y])),
	match(S1, ([X1,X2]-->[Y])),
	length(X1, N).
rule([cl,prop], inv, r(top), S, [], [r(N)]) :-
	match(S,  ([_X]-->[Y1,[top],_Y2])),
	length(Y1, N).
rule([cl,prop], inv, l(bot), S, [], [r(N)]) :-
	match(S,  ([X1,[bot],_X2]-->[_Y])),
	length(X1, N).
rule([cl,prop], inv, r(bot), S, [S1], [r(N),[]]) :-
	match(S,  ([X]-->[Y1,[bot],Y2])),
	match(S1, ([X]-->[Y1,Y2])),
	length(Y1, N).
% Rules for the propositional connectives
rule([cl,prop], inv, l(~), S, [S1], [l(N),r(0)]) :-
	match(S,  ([X1,[(~A)],X2]-->[Y])),
	match(S1, ([X1,X2]-->[[A],Y])),
	length(X1, N).
rule([cl,prop], inv, r(~), S, [S1], [r(N),l(0)]) :-
	match(S,  ([X]-->[Y1,[~A],Y2])),
	match(S1, ([[A],X]-->[Y1,Y2])),
	length(Y1, N).
rule([cl,prop], inv,  l(/\), S, [S1], [l(N),[l(N),l(N1)]]) :-
	match(S,  ([X1,[A/\B],X2]-->[Y])),
	match(S1, ([X1,[A,B],X2]-->[Y])),
	length(X1, N), N1 is N+1.
rule([cl,prop], inv,  r(\/), S, [S1], [r(N),[r(N),r(N1)]]) :-
	match(S,  ([X]-->[Y1,[A\/B],Y2])),
	match(S1, ([X]-->[Y1,[A,B],Y2])),
	length(Y1, N), N1 is N+1.
rule([cl,prop], inv, r(->), S, [S1], [r(N),[l(0),r(N)]]) :-
	match(S,  ([X]-->[Y1,[A->B],Y2])),
	match(S1, ([[A],X]-->[Y1,[B],Y2])),
	length(Y1, N).
rule([cl,prop], inv, r(/\), S, [S1, S2], [r(N),r(N),r(N)]) :-
	match(S,  ([X]-->[Y1,[A/\B],Y2])),
        match(S1, ([X]-->[Y1,[B],Y2])),
	match(S2, ([X]-->[Y1,[A],Y2])),
	length(Y1, N).
rule([cl,prop], inv, l(\/), S, [S1, S2], [l(N),l(N),l(N)]) :-
	match(S,  ([X1,[A\/B],X2]-->[Y])),
        match(S1, ([X1,[B],X2]-->[Y])),
	match(S2, ([X1,[A],X2]-->[Y])),
	length(X1, N).
rule([cl,prop], inv,  l(->), S, [S1, S2], [l(N),r(0),l(N)]) :-
	match(S,  ([X1,[A->B],X2]-->[Y])),
        match(S1, ([X1,[B],X2]-->[Y])),
	match(S2, ([X1,X2]-->[[A],Y])),
	length(X1, N).
% Rules for the quantifiers
rule([cl,first], no,  l(all), S, [S1], [l(N),[l(N),l(N1)]]) :-
	match(S,  ([X1,[V@A],X2]-->[Y])),
	substitute(V, _V1, A, A1),
	match(S1, ([X1,[A1,V@A],X2]-->[Y])),
	length(X1, N), N1 is N+1.
rule([cl,first], no, r(all), S, [S1], [r(N),r(N)]) :-
	match(S,  ([X]-->[Y1,[V@A],Y2])),
	substitute(V, V1, A, A1),
	match(S1, ([X]-->[Y1,[A1],Y2])),
	eigen_variable(V1, S),
	length(Y1, N).
rule([cl,first], no, l(exists), S, [S1], [l(N),l(N)]) :-
	match(S,  ([X1,[V#A],X2]-->[Y])),
	substitute(V, V1, A, A1),
	match(S1, ([X1,[A1],X2]-->[Y])),
	eigen_variable(V1, S),
	length(X1, N).
rule([cl,first], no,  r(exists), S, [S1], [r(N),[r(N),r(N1)]]) :-
	match(S,  ([X]-->[Y1,[V#A],Y2])),
	substitute(V, _V1, A, A1),
	match(S1, ([X]-->[Y1,[A1,V#A],Y2])),
	length(Y1, N), N1 is N+1.
% Cut rule
rule([cl,prop], no,  cut, S, [S1, S2], [[],r(0),l(0)]) :-
	match(S,  ([X]-->[Y])),
	match(S1, ([]-->[[C]])),
	match(S2, ([[C],X]-->[Y])).

match((X-->Y), (P-->Q)) :- append_all(P, X), append_all(Q, Y).

eigen_variable(V, X) :-
	freeze(V, fail),
	free_variables(X, Us),
	dif_list(Us, V).

free_variables(X, Vs) :- free_vars(X, [], [], Vs).

free_vars(X, BVs, Vs0, Vs) :- var(X), !, free_vars1(X, BVs, Vs0, Vs).
free_vars(X, _BVs, Vs, Vs) :- ground(X), !.
free_vars([X|Y], BVs, Vs0, Vs) :- !,
	free_vars(X, BVs, Vs0, Vs1), free_vars(Y, BVs, Vs1, Vs).
free_vars(all(X,A), BVs, Vs0, Vs) :- !,
	free_vars(A, [X|BVs], Vs0, Vs).
free_vars(exists(X,A), BVs, Vs0, Vs) :- !,
	free_vars(A, [X|BVs], Vs0, Vs).
free_vars(X, BVs, Vs0, Vs) :- X =.. Y, free_vars(Y, BVs, Vs0, Vs).

free_vars1(X, BVs, Vs, Vs) :- (memq(X, BVs); memq(X, Vs)), !.
free_vars1(X, _BVs, Vs, [X|Vs]).

dif_list([], _).
dif_list([U|Us], V) :- dif(U, V), dif_list(Us, V).

%%
%%  Standard form printer
%%
standard_print(P) :-
	standard_print(P, 0).

standard_print([Rule,_,S|Ps], Tab) :-
	tabx(Tab),
	write_rule_name(Rule), writex(': '), 
	write_seq(S), nlx,
	Tab1 is Tab+2,
	standard_print_list(Ps, Tab1).

standard_print_list([], _).
standard_print_list([P|Ps], Tab) :-
	standard_print(P, Tab), standard_print_list(Ps, Tab).
%%
%%  Pretty form printer
%%
pretty_print(P0) :-
	name_variables(P0, P),
	place_proof(P, [], Q, _, _),
	print_placed_proof(Q),
	fail.
pretty_print(_).

name_variables(X, Z) :-
	name_variables(X, 0, _N, [], _Vs, Z).

name_variables(X, N, N, Vs, Vs, X) :- ground(X), !.
name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !.
name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !,
	V is N0 mod 3, VN is N0//3,
	name_var(V, VN, Z),
	N is N0+1.
name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !,
	name_variables(X, N0, N1, Vs0, Vs1, Z),
	name_variables(Xs, N1, N, Vs1, Vs, Zs).
name_variables(X, N0, N, Vs0, Vs, Z) :-
	X =.. Xs,
	name_variables(Xs, N0, N, Vs0, Vs, Zs),
	Z =.. Zs.

name_var(0, VN, X) :- !, name_var1([0'X], VN, X).
name_var(1, VN, X) :- !, name_var1([0'Y], VN, X).
name_var(2, VN, X) :- !, name_var1([0'Z], VN, X).

name_var1([V], 0, X) :- !, name(X, [V]).
name_var1([V], VN, X) :-
	name(VN, Ns), 
	name(X, [V|Ns]).

%%
%%  place_proof(+Proof, +Margins, 
%%              -Proof_with_pos, -LowerLeftPos, -NewMargins)
%% 
place_proof([Rule,_,S|Ps1], Ms0, Q, LowerPos, Ms) :-
	get_margins([M0,M1|Ms1], Ms0),
	place_uppers(Ps1, Ms1, Ps2, UpperPos0, Ms2),
	get_margins([M2|_], Ms2),
	UpperWidth is M2-UpperPos0,
	get_rule_name_width(Rule, W1),
	get_seq_width(S, LowerWidth),
	LowerOff is max(0,max(UpperPos0,max(M1,M0))-UpperPos0),
	RulePos is UpperPos0+LowerOff,
	RuleWidth is max(UpperWidth,LowerWidth),
	LowerPos is RulePos+(RuleWidth-LowerWidth)//2,
	UpperPos is max(UpperPos0,RulePos),
	UpperOff is UpperPos-UpperPos0,
	move_proof_list(Ps2, UpperOff, Ps3),
	move_margins(Ms2, UpperOff, Ms3),
	new_rule_width(Rule, RuleWidth, W1, RuleWidth1, W2),
	Q = [RulePos+RuleWidth1,Rule,LowerPos+LowerWidth,S|Ps3],
	M11 is RulePos+RuleWidth1+W2,
	M01 is LowerPos+LowerWidth,
	Ms = [M01,M11|Ms3].

new_rule_width([_Rule,_], _, W1, 0, W1) :- !.
new_rule_width(_Rule, RW, W1, RW, W2) :- W2 is W1+1.

place_uppers(Ps, Ms0, Qs, T, Ms) :-
	place_proof_list(Ps, Ms0, Qs, T, Ms).

place_proof_list([], Ms0, [], T, Ms0) :- !,
	get_margins([T|_], Ms0).
place_proof_list([P1], Ms0, [Q1], T, Ms) :- !,
	place_proof(P1, Ms0, Q1, T, Ms).
place_proof_list([P1|Ps], Ms0, [Q1|Qs], T, Ms) :-
	place_proof(P1, Ms0, Q1, T, Ms1),
	move_margins(Ms1, 2, Ms2),
	place_proof_list(Ps, Ms2, Qs, _T1, Ms).

move_proof_list([], _, []).
move_proof_list([P0|Ps0], Off, [P|Ps]) :-
	move_proof(P0, Off, P),
	move_proof_list(Ps0, Off, Ps).

move_proof([M0+W0,Rule,M1+W1,S|Ps0], Off, [N0+W0,Rule,N1+W1,S|Ps]) :-
	N0 is M0+Off, N1 is M1+Off,
	move_proof_list(Ps0, Off, Ps).

get_margins(Zs, Xs) :- var(Zs), !, Zs=Xs.
get_margins([], _).
get_margins([Z|Zs], []) :- !, Z=0, get_margins(Zs, []).
get_margins([Z|Zs], [Z|Xs]) :- get_margins(Zs, Xs).

move_margins([], _, []).
move_margins([M0|Ms0], Off, [M|Ms]) :-
	M is M0+Off, move_margins(Ms0, Off, Ms).

%%
%%  print_placed_proof(+Placed_Proof)
%%
print_placed_proof(P) :-
	print_placed_proofs([P]).

print_placed_proofs([]).
print_placed_proofs(Ps) :- Ps=[_|_],
	gather_uppers(Ps, Qs),
	print_placed_proofs(Qs),
	print_rules(Ps),
	nlx,
	print_lowers(Ps),
	nlx.

gather_uppers([], []).
gather_uppers([P|Ps], Qs) :-
	gather_uppers(Ps, Qs1),
	P = [_,_Rule,_,_S|P0],
	append(P0, Qs1, Qs).

print_rules([]).
print_rules([P|Ps]) :-
	P = [M0+W0,Rule,_M1+_W1,_S|_],
	goto_pos(M0),
	print_rule_line(W0),
	write_rule_name(Rule),
	print_rules(Ps).

print_rule_line(0) :- !.
print_rule_line(N) :- N>0, n_writex(N, '-'), writex(' ').

print_lowers([]).
print_lowers([P|Ps]) :-
	P = [_M0+_W0,_Rule,M1+_W1,S|_],
	goto_pos(M1),
	write_seq(S),
	print_lowers(Ps).

get_width(X, W) :-
	open_null(NULL, OldSTR, OldLog),
	nlx,
	writex(X),
	line_position(W),
	close_null(NULL, OldSTR, OldLog).

get_rule_name_width(R, W) :-
	open_null(NULL, OldSTR, OldLog),
	nlx,
	write_rule_name(R),
	line_position(W),
	close_null(NULL, OldSTR, OldLog).

get_seq_width(S, W) :-
	open_null(NULL, OldSTR, OldLog),
	nlx,
	write_seq(S),
	line_position(W),
	close_null(NULL, OldSTR, OldLog).

open_null(NULL, OldSTR, OldLog) :-
	current_output(OldSTR),
	open_null_stream(NULL),
	set_output(NULL),
	log_suspend(OldLog).

close_null(NULL, OldSTR, OldLog) :-
	close(NULL),
	set_output(OldSTR),
	log_resume(OldLog).

write_rule_name(axiom) :- !, writex('Axiom').
write_rule_name(ax) :- !, writex('Ax').
write_rule_name(cut) :- !, writex('Cut').
write_rule_name(r(all)) :- !, writex('R@').
write_rule_name(r(exists)) :- !, writex('R#').
write_rule_name(r(R)) :- !, writex('R'), writex(R).
%write_rule_name(r(R,N)) :- !, writex('R'), writex(R), writex(N).
write_rule_name(l(all)) :- !, writex('L@').
write_rule_name(l(exists)) :- !, writex('L#').
write_rule_name(l(R)) :- !, writex('L'), writex(R).
%write_rule_name(l(R,N)) :- !, writex('L'), writex(R), writex(N).

write_seq((Xs-->Ys)) :-
	write_list(Xs), writex(' --> '), write_list(Ys).
	
write_list([]).
write_list([X]) :- !, writex(X).
write_list([X|Xs]) :- writex(X), writex(','), write_list(Xs).


%%  BUSSPROOFS section 
%%  LaTeX Printer for   bussproofs.sty
%%

buss_tex_print(P) :-
        writex('\\begin{prooftree}\n'), 
	buss_tex_name_variables(P, Q),
	buss_tex_print(0, Q),
        writex('\n\\end{prooftree}\n').

buss_tex_name_variables(X, Z) :-
	buss_tex_name_variables(X, 0, _N, [], _Vs, Z).

buss_tex_name_variables(X, N, N, Vs, Vs, X) :- ground(X), !.
buss_tex_name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !.
buss_tex_name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !,
	V is N0 mod 3, VN is N0//3,
	buss_tex_name_var(V, VN, Z),
	N is N0+1.
buss_tex_name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !,
	buss_tex_name_variables(X, N0, N1, Vs0, Vs1, Z),
	buss_tex_name_variables(Xs, N1, N, Vs1, Vs, Zs).
buss_tex_name_variables(X, N0, N, Vs0, Vs, Z) :-
	X =.. Xs,
	buss_tex_name_variables(Xs, N0, N, Vs0, Vs, Zs),
	Z =.. Zs.

buss_tex_name_var(0, VN, X) :- !, buss_tex_name_var1([0'x], VN, X).
buss_tex_name_var(1, VN, X) :- !, buss_tex_name_var1([0'y], VN, X).
buss_tex_name_var(2, VN, X) :- !, buss_tex_name_var1([0'z], VN, X).

buss_tex_name_var1([V], 0, X) :- !, name(X, [V]).
buss_tex_name_var1([V], VN, X) :-
	name(VN, Ns), append(Ns, [0'}], Ns1),
	name(X, [V,0'_,0'{|Ns1]).

buss_tex_print(Tab, [[Rule, _], _, S]) :- !,
        tabx(Tab),
    (buss_tex_is_branching(Rule) ->  % 
        writex('\\BinaryInfC{$');
        writex('\\UnaryInfC{$')),
    buss_tex_print_sequent(S),
    writex('$}\n'),
    tabx(Tab),
    (Rule = ax -> % Check if the rule is Ax
            writex('\\RightLabel{$Ax.$}\n\\AxiomC{}')
        ;
            writex('\\RightLabel{$'),
            buss_tex_print_rule_name(Rule),
            writex('$}')
    ),
    buss_tex_print_list(_Ss, Tab).

buss_tex_print(Tab, [Rule, _, S | Ss]) :-
    tabx(Tab),
    (buss_tex_is_branching(Rule) ->  % 
        writex('\\BinaryInfC{$');
        writex('\\UnaryInfC{$')),
    buss_tex_print_sequent(S),
    writex('$}\n'),
    tabx(Tab),
    (Rule = ax -> % Check if the rule is Ax
            writex('\\RightLabel{$Ax.$}\n\\AxiomC{}')
        ;
            writex('\\RightLabel{$'),
            buss_tex_print_rule_name(Rule),
            writex('$}')
    ),
    buss_tex_print_list(Ss, Tab).

buss_tex_print_list([], _Tab).
buss_tex_print_list([S1], Tab) :- !,
	nlx,
	Tab1 is Tab+2,
	buss_tex_print(Tab1, S1),
	tabx(Tab).
buss_tex_print_list([S1|Ss], Tab) :- !,
	nlx,
	Tab1 is Tab+2,
	buss_tex_print(Tab1, S1),
	tabx(Tab1),
	buss_tex_print_list(Ss, Tab).

buss_tex_print_sequent((Xs-->Ys)) :-
	buss_tex_print_formulas(Xs),
	writex(' \\vdash '),
	buss_tex_print_formulas(Ys).

buss_tex_print_formulas([]).
buss_tex_print_formulas([A]) :- !,
	buss_tex_print_formula(A).
buss_tex_print_formulas([A|As]) :-
	buss_tex_print_formula(A),
	writex(', '),
	buss_tex_print_formulas(As).

buss_tex_print_formula(A) :-
	buss_tex_print_formula(999, A).

buss_tex_print_formula(Prec0, A) :- buss_tex_quantifier_name(A, Q, X, B), !,
	Prec = 999,
	(Prec0 < Prec -> writex('('); true),
	writex(Q), writex(' '), writex(X), writex('.'),
	buss_tex_print_formula(B),
	(Prec0 < Prec -> writex(')'); true),
	!.
buss_tex_print_formula(Prec0, A) :- is_op(A, Prec, Type, Op, As), !,
	(Prec0 < Prec -> writex('('); true),
	buss_tex_print_op_formula(Prec, Type, Op, As),
	(Prec0 < Prec -> writex(')'); true),
	!.
buss_tex_print_formula(_Prec0, A) :- buss_tex_unit_name(A, U), !,
	writex(U).
buss_tex_print_formula(_Prec0, A) :-
	rename_functor(A, A1),
	writex(A1).

rename_functor(X, Z) :-
	X =.. [F0|As],
	capitalize_atom(F0, F),
	Z =.. [F|As].

buss_tex_quantifier_name(X@A, '\\forall', X, A).
buss_tex_quantifier_name(X#A, '\\exists', X, A).

buss_tex_unit_name(_, _) :- fail.
buss_tex_unit_name(bot, '\\bot').
buss_tex_unit_name(top, '\\top').

%buss_tex_print_op_formula(Prec, fy, Op, [A1]) :- Op = ~, !,
%	buss_tex_print_op(Op), writex('{'),
%	buss_tex_print_formula(Prec, A1), writex('}').
buss_tex_print_op_formula(Prec, fx, Op, [A1]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_op(Op), writex(' '),
	buss_tex_print_formula(Prec1, A1).
buss_tex_print_op_formula(Prec, fy, Op, [A1]) :- !,
	buss_tex_print_op(Op), writex(' '),
	buss_tex_print_formula(Prec, A1).
buss_tex_print_op_formula(Prec, xf, Op, [A1]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	writex(' '), buss_tex_print_op(Op).
buss_tex_print_op_formula(Prec, yf, Op, [A1]) :- !,
	buss_tex_print_formula(Prec, A1),
	writex(' '), buss_tex_print_op(Op).
buss_tex_print_op_formula(Prec, xfx, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	writex(' '), buss_tex_print_op(Op), writex(' '),
	buss_tex_print_formula(Prec1, A2).
buss_tex_print_op_formula(Prec, xfy, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	writex(' '), buss_tex_print_op(Op), writex(' '),
	buss_tex_print_formula(Prec, A2).
buss_tex_print_op_formula(Prec, yfx, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec, A1),
	writex(' '), buss_tex_print_op(Op), writex(' '),
	buss_tex_print_formula(Prec1, A2).

is_op(A, Prec, Type, Op, As) :-
	functor(A, Op, N), current_op(Prec, Type, Op),
	is_op0(A, Type, N, As),
	!.
is_op0(A, fx, 1, [A1]) :- arg(1, A, A1).
is_op0(A, fy, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, yf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, xfy, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, yfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).

buss_tex_print_op(Op) :-
	buss_tex_op_name(Op, OpName), !,
	writex(OpName).

buss_tex_op_name(~,  '\\lnot').
buss_tex_op_name(/\, '\\land').
buss_tex_op_name(\/, '\\lor').
buss_tex_op_name(->, '\\to').

buss_tex_print_rule_name([Rule,LN]) :- !,
	buss_tex_rule_name(Rule, RuleName),
	!,
	writex(RuleName),
	writex('('), writex(LN), writex(')').
buss_tex_print_rule_name(Rule) :-
	buss_tex_rule_name(Rule, RuleName),
	!,
	writex(RuleName).

buss_tex_rule_name(ax, 'Ax').
buss_tex_rule_name(axiom, 'Axiom').
buss_tex_rule_name(l(top), 'L\\top').
buss_tex_rule_name(r(top), 'R\\top').
buss_tex_rule_name(l(bot), 'L\\bot').
buss_tex_rule_name(r(bot), 'R\\bot').
buss_tex_rule_name(l(~), 'L\\lnot').
buss_tex_rule_name(r(~), 'R\\lnot').
buss_tex_rule_name(l(/\), 'L\\land').
buss_tex_rule_name(r(/\), 'R\\land').
buss_tex_rule_name(l(\/), 'L\\lor').
buss_tex_rule_name(r(\/), 'R\\lor').
buss_tex_rule_name(l(->), 'L\\to').
buss_tex_rule_name(r(->), 'R\\to').
buss_tex_rule_name(l(all), 'L\\forall').
buss_tex_rule_name(r(all), 'R\\forall').
buss_tex_rule_name(l(exists), 'L\\exists').
buss_tex_rule_name(r(exists), 'R\\exists').
buss_tex_rule_name(cut, 'Cut').

buss_tex_is_branching(r(/\)).
buss_tex_is_branching(l(\/)).
buss_tex_is_branching(l(->)).

%% End of bussproofs printer. 
%%
%%
%%  Utilities
%%
append_all([], []).
append_all([P], P).
append_all([P|Ps], X) :- Ps=[_|_], append(P, X1, X), append_all(Ps, X1).

merge(X1, X2, X) :- split(X, X1, X2).

split([], [], []).
split([X|Xs], [X|Ys], Zs) :- split(Xs, Ys, Zs).
split([X|Xs], Ys, [X|Zs]) :- split(Xs, Ys, Zs).

append([], Z, Z).
append([W|X], Y, [W|Z]) :- append(X, Y, Z).

member(X, [X|_Xs]).
member(X, [_Y|Xs]) :- member(X, Xs).

memberq(X, [X|_Xs]) :- !.
memberq(X, [_Y|Xs]) :- memberq(X, Xs).

memq(X, [Y|_Xs]) :- X==Y, !.
memq(X, [_Y|Xs]) :- memq(X, Xs).

get_nth(0, [X|_Xs], X) :- !.
get_nth(N, [_|Xs], X) :- N>0, N1 is N-1, get_nth(N1, Xs, X).

for(I, M, N) :- M =< N, I=M.
for(I, M, N) :- M =< N, M1 is M+1, for(I, M1, N).

assoc(X, Z, [[X0|Z]|_As]) :- X==X0, !.
assoc(X, Z, [_|As]) :- assoc(X, Z, As).

substitute(X0, X, A0, A) :- var(A0), X0==A0, !, A=X.
substitute(_X0, _X, A0, A) :- var(A0), !, A=A0.
substitute(_X0, _X, A0, A) :- atomic(A0), !, A=A0.
substitute(X0, X, [A0|B0], [A|B]) :- !,
	substitute(X0, X, A0, A),
	substitute(X0, X, B0, B).
substitute(X0, X, A0, A) :-
	A0 =.. B0,
	substitute(X0, X, B0, B),
	A =.. B.

capitalize_atom(X, Z) :- atom(X),
	name(X, [C0|Cs]), C0 >= 0'a, C0 =< 0'z, !,
	C is ((C0 - 0'a) + 0'A),
	name(Z, [C|Cs]).
capitalize_atom(X, X).

n_writex(0, _) :- !.
n_writex(N, X) :- N>0, writex(X), N1 is N-1, n_writex(N1, X).

flush_out :-
	current_output(S),
	flush_output(S).

goto_pos(T) :-
	current_output(S),
	line_position(S, T0),
	tabx(T-T0).

line_position(W) :-
	current_output(S),
	line_position(S, W).

%%
%%  Logging
%%
log_start(yes) :- !,
	log_start('seqprover.log').
log_start(File) :-
	logging(no, _),
	!,
	open(File, write, STR),
	retractall(logging(_,_)),
	assert(logging(File, STR)).

log_end :-
	logging(no, _),
	!.
log_end :-
	logging(_File, STR),
	close(STR),
	fail.
log_end :-
	retractall(logging(_,_)),
	assert(logging(no, _)).

log_suspend(logging(File,STR)) :-
	logging(File, STR),
	retractall(logging(_,_)),
	assert(logging(no, _)).

log_resume(logging(File,STR)) :-
	retractall(logging(_,_)),
	assert(logging(File, STR)).

readx(STR, X) :-
	read(STR, X),
	echo_read(STR, X).

echo_read(user_input, _X) :-
	logging(no, _),
	!.
echo_read(user_input, X) :-
	logging(_File, STR),
	!,
	write(STR, X),
	write(STR, '.'),
	nl(STR).
echo_read(_, X) :-
	writex(X),
	writex('.'),
	nlx.

writex(X) :-
	logging(no, _),
	!,
	write(X).
writex(X) :-
	logging(_, STR),
	write(X),
	write(STR, X).

nlx :-
	logging(no, _),
	!,
	nl.
nlx :-
	logging(_, STR),
	nl,
	nl(STR).

tabx(X) :-
	logging(no, _),
	!,
	tab(X).
tabx(X) :-
	logging(_, STR),
	tab(X),
	tab(STR, X).

%%
%%  Batch
%%
batch :-
	nl, write('# Start'), nl,
	% prolog_flag(syntax_errors, _, quiet),
	read(Output),
	read(Sequent),
	set_output_form(Output),
	batch_prove(Sequent),
	!,
	flush_out,
	halt.
batch :-
	nl, write('# Syntax error'), nl,
	flush_out,
	halt.

batch_prove((X <--> Y)) :- !,
	batch_prove((X --> Y)),
	nl,
	batch_prove((Y --> X)).
batch_prove(S0) :-
	(
	    convert_to_seq(S0, S),
	    sequentq(S)
	;
	    formulaq(S0),
	    S = ([] --> [S0])
	),
	!,
        write('# Proving '), write(S), nl,
	statistics(runtime, _),
	(prove(S, P) ->
	    statistics(runtime, [_,T]),
	    nl,
            write('# BEGIN Proof'), nl,
	    print_proof(P),
            nl, write('# END Proof'), nl,
	    nl, write('# Proved in '),
	    write(T), write(' msec.'), nl
	;
	    nl, write('# Fail to prove'), nl
	).

%%
%%  Initialization
%%
:- seq_init.

Sorry for this long code quotation. After consult, enter "prover . " and then "output(buss) . "
Example:

?- prover. 
Sequent Calculus Prover ver 2.0 in Prolog
        by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cl(first)> output(buss).
output(buss).
yes
cl(first)> top --> ~ a \/ a . 
top--> ~a\/a.
Trying to prove with threshold = 0
Succeed in proving top --> ~a\/a (1 msec.)
buss:1 =
\begin{prooftree}
\UnaryInfC{$\top \vdash \lnot A \lor A$}
\RightLabel{$L\top$}
  \UnaryInfC{$ \vdash \lnot A \lor A$}
  \RightLabel{$R\lor$}
    \UnaryInfC{$ \vdash \lnot A, A$}
    \RightLabel{$R\lnot$}
      \UnaryInfC{$A \vdash A$}
      \RightLabel{$Ax.$}
\AxiomC{}      
\end{prooftree}
yes

Once the proofs would be put in the reverse order inside \begin{prooftree} … \end{prooftree} the main work will be done. Thanks for your help.

Thanks @j4n_bur53 , I am going to inspect all the writing occurrences in this file to test this solution.

@j4n_bur53 , your solution was the right one, many thanks. The problem is solved and I will soon paste the code here after minor corrections.

Here is the code of seqprover.pl . This prover works only with bussproofs.sty . It is a simplified version of Naoyuki’s prover :

%%%
%%%  Sequent Calculus Prover in Prolog
%%%  by Naoyuki Tamura (tamura@kobe-u.ac.jp)
%%%  TeX form output by Eiji Sugiyama
%%%
%%%  You can freely distribute or modify this program.
%%%
%%%  Version 2.0
%%%    12/30/2020 Modified for SWI Prolog
%%%
:- dynamic
	seq_system/2, threshold/1, output_form/1, logging/2,
	output_count/1, output_result/2,
	proved/3, not_proved/2, axiom/1.
%seq_system(cl,first).
%threshold(5).
%output_form(pretty).
%logging(no, _).
%output_count(1).

:- op(1200, xfx, [ -->, <--> ]).
:- op( 900, xfy, [ -> ]).
% :- op( 850, xfy, [ -> ]).
:- op( 850, xfy, [ /\, \/ ]).
:- op( 800, fy,  [ ~ ]).
:- op( 750, xfy, [ @, # ]).

prover :-
	write('Sequent Calculus Prover ver 2.0 in Prolog'), nl,
	write('        by Naoyuki Tamura (tamura@kobe-u.ac.jp)'), nl,
%	seq_init,
	statistics(runtime, [T0,_]),
	seq_prover,
	statistics(runtime, [T1,_]),
	T is T1-T0,
	write('Exit from Sequent Calculus Prover...'), nl,
	write('Total CPU time = '), write(T), write(' msec.'), nl,
	log_end.

seq_init :-
	set_system(cl,first),
	set_threshold(5),
	set_axioms([]),
	set_output_form(buss),
	log_end,
	reset_output_result.

seq_prover :-
	current_input(STR),
	seq_prover(STR).

seq_prover(STR) :-
        prompt(_, ''),
	repeat,
	  seq_system(Sys, Opt),
	  write(Sys), write('('), write(Opt), write(')'),
	  write('> '),
          flush_out,
	  readx(STR, X),
	  seq_command(X),
	seq_quit(X),
	close(STR).

seq_quit(X) :-
	nonvar(X),
	memberq(X, [quit, end, bye, halt, end_of_file]).

seq_command(X) :-
	seq_execute(X),
	!,
	write(yes), nl.
seq_command(_) :-
	write(no), nl.

seq_execute(X) :- var(X), !, fail.
seq_execute(X) :- seq_quit(X), !.
seq_execute(help) :- !, seq_help.
seq_execute(init) :- !, seq_init.
seq_execute([File]) :- !, seq_consult(File).
seq_execute(cl(Opt)) :- !, set_system(cl,Opt).
%seq_execute(il(Opt)) :- !, set_system(il,Opt).
seq_execute(threshold(N)) :- var(N), !,
	threshold(N),
	write(threshold(N)), nl.
seq_execute(threshold(N)) :- !,
	set_threshold(N).
seq_execute(axioms(As)) :- var(As), !,
	(bagof(A, axiom(([]-->[A])), As); As=[]), !,
	write(axioms(As)), nl.
seq_execute(axioms(As)) :- !,
	set_axioms(As).
seq_execute(output(Form)) :- var(Form), !,
	output_form(Form),
	write(output(Form)). %nl.
seq_execute(output(Form)) :-
	set_output_form(Form).
seq_execute(log(File)) :- var(File), !,
	logging(File, _),
	write(log(File)), nl.
seq_execute(log(no)) :- !,
	log_end.
seq_execute(log(File)) :- !,
	log_start(File).
seq_execute(N) :- integer(N), !,
	get_output_result(N, N1, P),
	print_output(N1, P).
seq_execute((Xs <--> Ys)) :- !,
	seq_execute((Xs --> Ys)),
	seq_execute((Ys --> Xs)).
seq_execute((Xs --> Ys)) :-
	convert_to_seq((Xs --> Ys), Seq),
	sequentq(Seq),
	!,
	seq_prove(Seq).
seq_execute(X) :-
	write('Error '),
	write(X),
	write(' is not a command nor a sequent.'), nl.

seq_help :-
	write('A1,...,Am -->  B1,...,Bn : Try to prove the sequent.'), nl,
	write('A1,...,Am <--> B1,...,Bn : Try to prove the sequent '),
	    write('in both directions.'), nl,
	write('help           : Help.'), nl,
	write('init           : Initialize the prover.'), nl,
	write('[File]         : Read from the file.'), nl,
	write('Sys(Opt)       : Select the system. '),
	    write('Sys={cl}, Opt={first|prop}'), nl,
	write('threshold(N)   : Set/retrieve the threshold. N>=0'), nl,
	write('axioms(Axioms) : Set/retrieve the axioms. '), 
	    write('Axioms=[A1,...,Am]'), nl,
	write('output(Form)   : Set/retrieve the output form. '), 
	    write('Form={pretty|tex|standard|term}'), nl,
	write('log(L)         : Start/stop/retrieve the output logging. '), 
	    write('L={yes|File|no}'), nl,
	write('N              : Display the N-th output.'), nl,
	write('quit           : Quit.'), nl.

seq_consult(File) :-
	open(File, read, STR),
	seq_prover(STR).

seq_prove(Seq) :-
	statistics(runtime,[_,_]),
	prove(Seq, Proof),
	statistics(runtime,[_,Time]),
	write('Succeed in proving '), 
	% write_seq(Seq),
	write(' ('), write(Time), write(' msec.)'),
	output_count(N),
        nl,
	assert_output_result(Proof),
	!,
	print_output(N, Proof).
seq_prove(_Seq) :-
	statistics(runtime,[_,Time]),
	write('Fail to prove '),
	% write_seq(Seq),
	write(' ('), write(Time), write(' msec.)'), nl.

print_output(N, P) :-
	output_form(Form), write(Form), write(':'),
	write(N), write(' ='), nl,nl,
	print_proof(P).

print_proof(P) :-
	output_form(Form),
	print_proof_form(Form, P).

print_proof_form(pretty, P) :- !,
	pretty_print(P).

print_proof_form(tex, P) :- !,
	tex_print(P).

print_proof_form(buss, P) :- !,
	buss_tex_print(P).

print_proof_form(standard, P) :- !,
	standard_print(P).
print_proof_form(term, P) :- !,
	write(P). %nl.

set_system(Sys, Opt) :-
	memberq(Sys, [cl]),
	memberq(Opt, [prop,first]),
	retractall(seq_system(_,_)),
	assert(seq_system(Sys,Opt)).

set_threshold(N) :-
	integer(N), N >= 0,
	retractall(threshold(_)),
	assert(threshold(N)).

set_axioms(Axioms) :-
	retractall(axiom(_)),
	assert_axioms(Axioms).

assert_axioms([]).
assert_axioms([A|As]) :-
	formulaq(A),
	!,
	assert(axiom(([]-->[A]))),
	assert_axioms(As).
assert_axioms([A|As]) :-
	write('Error '), write(A),
	write(' is not a formula.'), nl,
	assert_axioms(As).

set_output_form(Form) :-
	memberq(Form, [buss, pretty, tex, standard, term]),
	retractall(output_form(_)),
	assert(output_form(Form)).

reset_output_result :-
	retractall(output_count(_)),
	retractall(output_result(_,_)),
	assert(output_count(1)).

assert_output_result(P) :-
	output_count(N),
	assert(output_result(N,P)),
	retractall(output_count(_)),
	N1 is N+1,
	assert(output_count(N1)).

get_output_result(N, N, P) :- N>0, !,
	output_result(N, P).
get_output_result(N, N1, P) :-
	output_count(M),
	N1 is M+N,
	output_result(N1, P).

convert_to_seq((Xs --> Ys), (Xs1 --> Ys1)) :-
	convert_to_list(Xs, Xs1), convert_to_list(Ys, Ys1).

convert_to_list(X, _) :- var(X), !, fail.
convert_to_list([], []) :- !.
convert_to_list([X|Xs], [X|Xs]) :- !.
convert_to_list((X,Xs), [X|Zs]) :- !, convert_to_list(Xs, Zs).
convert_to_list(X, [X]).

sequentq((X-->Y)) :- formula_listq(X), formula_listq(Y).

formula_listq([]).
formula_listq([A|As]) :- formulaq(A), formula_listq(As).

formulaq(A) :- var(A), !, fail.
formulaq((_-->_)) :- !, fail.
formulaq([]) :- !, fail.
formulaq([_|_]) :- !, fail.
formulaq(~A) :- !, formulaq(A).
formulaq(A/\B) :- !, formulaq(A), formulaq(B).
formulaq(A\/B) :- !, formulaq(A), formulaq(B).
formulaq(A->B) :- !, formulaq(A), formulaq(B).
formulaq(_X@A) :- !, formulaq(A).
formulaq(_X#A) :- !, formulaq(A).
formulaq(_).

%%
%%  Sequent Calculus Prover
%%
%%  seq_system( {cl}, {prop|first} ).
%%    seq_system(cl,first).
%%  Max number of cut and contraction rules: cut, r(all), l(exists)
%%    threshold(5).
%%  Axioms
%%    axiom(Ax1). axiom(Ax2). ....

prove(S, P) :-
	retractall(proved(_,_,_)),
	retractall(not_proved(_,_)),
	threshold(N),
	write('Trying to prove with threshold ='),
	for(I, 0, N),
	% write(' '),
        write(I),
	flush_out,
	prove(S, P, I),
         nl,
	!.
prove(_S, _P) :-
	nl,
	fail.

prove(S, _P, N) :-
	ground(S),
	clause(not_proved(S,M), _),
	N =< M,
	!,
	fail.
prove(S, P, N) :-
	ground(S),
	clause(proved(S,P,M), _),
	M =< N,
	!.
prove(S, P, _N) :-
	clause(axiom(S), _),
	P = [axiom,[[]],S],
	!.
prove(S, P, N) :-
	check_sequent(S),
	select_rule(Rule, S, Ss, Pos),
	P = [Rule,Pos,S|Ps],
	set_sequents(Ss, Ps),
	rule_constraint(Rule, Ps, M),
	N1 is N-M, N1 >= 0,
       	prove_all(Ss, Ps, N1),
%	!,
	assert(proved(S,P,N)).
prove(S, _P, N) :-
	ground(S),
	assert(not_proved(S,N)),
	!,
	fail.

prove_all([], [], _N).
prove_all([S|Ss], [P|Ps], N) :-
	prove(S, P, N),
	prove_all(Ss, Ps, N).

check_sequent((X-->Y)) :-
	length(X, N1), length(Y, N2),
	N1 + N2 < 20.
%check_sequent(_) :- seq_system(cl,_), !.
%check_sequent((_X-->Y)) :- (Y=[]; Y=[_]), !.

select_rule(Rule, S, Ss, Pos) :-
	rule(RuleSys, inv, Rule, S, Ss, Pos),
	check_rule(RuleSys),
	!.
select_rule(Rule, S, Ss, Pos) :-
	rule(RuleSys, no, Rule, S, Ss, Pos),
	check_rule(RuleSys).

check_rule([RSys,ROp]) :-
	seq_system(Sys, Op),
	check_rule1(Sys, RSys),
	check_rule2(Op, ROp),
	!.

check_rule1(Sys, Sys).
check_rule1(cl, _).

check_rule2(Op, Op).
check_rule2(first, _).

set_sequents([], []).
set_sequents([S|Ss], [[_,_,S|_]|Ps]) :- set_sequents(Ss, Ps).

rule_constraint(cut, [P1,_P2], 1) :- !,
	axiom(S1),
	P1 = [axiom,_,S1].
% bug report from Joseph Vidal-Rosset
rule_constraint(l(all), [P1], 1) :- !,
	P1 = [NextRule,_,_|_],
	dif(NextRule, l(all)).
rule_constraint(r(exists), [P1], 1) :- !,
	P1 = [NextRule,_,_|_],
	dif(NextRule, r(exists)).
rule_constraint(_Rule, _, 0).

% Logical axiom
% cannot be invertible owing to unification
rule([cl,prop], no, ax, S, [], [[]]) :-
	match(S,  ([_X1,[A],_X2]-->[_Y1,[B],_Y2])),
        unify_with_occurs_check(A,B).
% Rules for the propositional constants
rule([cl,prop], inv, l(top), S, [S1], [l(N),[]]) :-
	match(S,  ([X1,[top],X2]-->[Y])),
	match(S1, ([X1,X2]-->[Y])),
	length(X1, N).
rule([cl,prop], inv, r(top), S, [], [r(N)]) :-
	match(S,  ([_X]-->[Y1,[top],_Y2])),
	length(Y1, N).
rule([cl,prop], inv, l(bot), S, [], [r(N)]) :-
	match(S,  ([X1,[bot],_X2]-->[_Y])),
	length(X1, N).
rule([cl,prop], inv, r(bot), S, [S1], [r(N),[]]) :-
	match(S,  ([X]-->[Y1,[bot],Y2])),
	match(S1, ([X]-->[Y1,Y2])),
	length(Y1, N).
% Rules for the propositional connectives
rule([cl,prop], inv, l(~), S, [S1], [l(N),r(0)]) :-
	match(S,  ([X1,[(~A)],X2]-->[Y])),
	match(S1, ([X1,X2]-->[[A],Y])),
	length(X1, N).
rule([cl,prop], inv, r(~), S, [S1], [r(N),l(0)]) :-
	match(S,  ([X]-->[Y1,[~A],Y2])),
	match(S1, ([[A],X]-->[Y1,Y2])),
	length(Y1, N).
rule([cl,prop], inv,  l(/\), S, [S1], [l(N),[l(N),l(N1)]]) :-
	match(S,  ([X1,[A/\B],X2]-->[Y])),
	match(S1, ([X1,[A,B],X2]-->[Y])),
	length(X1, N), N1 is N+1.
rule([cl,prop], inv,  r(\/), S, [S1], [r(N),[r(N),r(N1)]]) :-
	match(S,  ([X]-->[Y1,[A\/B],Y2])),
	match(S1, ([X]-->[Y1,[A,B],Y2])),
	length(Y1, N), N1 is N+1.
rule([cl,prop], inv, r(->), S, [S1], [r(N),[l(0),r(N)]]) :-
	match(S,  ([X]-->[Y1,[A->B],Y2])),
	match(S1, ([[A],X]-->[Y1,[B],Y2])),
	length(Y1, N).
rule([cl,prop], inv, r(/\), S, [S1, S2], [r(N),r(N),r(N)]) :-
	match(S,  ([X]-->[Y1,[A/\B],Y2])),
        match(S1, ([X]-->[Y1,[A],Y2])),
        match(S2, ([X]-->[Y1,[B],Y2])),
	length(Y1, N).
rule([cl,prop], inv, l(\/), S, [S1, S2], [l(N),l(N),l(N)]) :-
	match(S,  ([X1,[A\/B],X2]-->[Y])),
       	match(S1, ([X1,[A],X2]-->[Y])),
        match(S2, ([X1,[B],X2]-->[Y])),
	length(X1, N).
rule([cl,prop], inv,  l(->), S, [S1, S2], [l(N),r(0),l(N)]) :-
	match(S,  ([X1,[A->B],X2]-->[Y])),
        match(S1, ([X1,X2]-->[[A],Y])),
        match(S2, ([X1,[B],X2]-->[Y])),
	length(X1, N).
% Rules for the quantifiers
rule([cl,first], no,  l(all), S, [S1], [l(N),[l(N),l(N1)]]) :-
	match(S,  ([X1,[V@A],X2]-->[Y])),
	substitute(V, _V1, A, A1),
	match(S1, ([X1,[A1,V@A],X2]-->[Y])),
	length(X1, N), N1 is N+1.
rule([cl,first], no, r(all), S, [S1], [r(N),r(N)]) :-
	match(S,  ([X]-->[Y1,[V@A],Y2])),
	substitute(V, V1, A, A1),
	match(S1, ([X]-->[Y1,[A1],Y2])),
	eigen_variable(V1, S),
	length(Y1, N).
rule([cl,first], no, l(exists), S, [S1], [l(N),l(N)]) :-
	match(S,  ([X1,[V#A],X2]-->[Y])),
	substitute(V, V1, A, A1),
	match(S1, ([X1,[A1],X2]-->[Y])),
	eigen_variable(V1, S),
	length(X1, N).
rule([cl,first], no,  r(exists), S, [S1], [r(N),[r(N),r(N1)]]) :-
	match(S,  ([X]-->[Y1,[V#A],Y2])),
	substitute(V, _V1, A, A1),
	match(S1, ([X]-->[Y1,[A1,V#A],Y2])),
	length(Y1, N), N1 is N+1.
% Cut rule
rule([cl,prop], no,  cut, S, [S1, S2], [[],r(0),l(0)]) :-
	match(S,  ([X]-->[Y])),
	match(S1, ([]-->[[C]])),
	match(S2, ([[C],X]-->[Y])).

match((X-->Y), (P-->Q)) :-
         append_all(Q, Y),
         append_all(P, X).
       

eigen_variable(V, X) :-
	freeze(V, fail),
	free_variables(X, Us),
	dif_list(Us, V).

free_variables(X, Vs) :- free_vars(X, [], [], Vs).

free_vars(X, BVs, Vs0, Vs) :- var(X), !, free_vars1(X, BVs, Vs0, Vs).
free_vars(X, _BVs, Vs, Vs) :- ground(X), !.
free_vars([X|Y], BVs, Vs0, Vs) :- !,
	free_vars(X, BVs, Vs0, Vs1), free_vars(Y, BVs, Vs1, Vs).
free_vars(all(X,A), BVs, Vs0, Vs) :- !,
	free_vars(A, [X|BVs], Vs0, Vs).
free_vars(exists(X,A), BVs, Vs0, Vs) :- !,
	free_vars(A, [X|BVs], Vs0, Vs).
free_vars(X, BVs, Vs0, Vs) :- X =.. Y, free_vars(Y, BVs, Vs0, Vs).

free_vars1(X, BVs, Vs, Vs) :- (memq(X, BVs); memq(X, Vs)), !.
free_vars1(X, _BVs, Vs, [X|Vs]).


dif_list([], _).
dif_list([U|Us], V) :-
        dif(U, V),
        dif_list(Us, V).
%%
%%  BUSSPROOFS section 
%%  LaTeX Printer for   bussproofs.sty
%%

buss_tex_print(P) :-
         buss_tex_name_variables(P, Q),
        write('\\begin{prooftree}\n\\def\\fCenter{\\mbox{\\ $\\vdash$\\ }}\n'), 
	buss_tex_print(0, Q),
        write('\n\\end{prooftree}\n\n').
buss_tex_print(Tab, [Rule, _, S | Ss]) :- 
         buss_tex_print_list(Ss, Tab),
    (Rule = ax -> % Check if the rule is Ax
            write('\\AxiomC{}\\RightLabel{$Ax.$}\n')
        ;
            write('\\RightLabel{$'),
            buss_tex_print_rule_name(Rule),
            write('$}\n')
    ),!,
    (buss_tex_is_branching(Rule) ->  % 
        write('\\BinaryInf$');
        write('\\UnaryInf$')),
    buss_tex_print_sequent(S),
    write('$').
/*
buss_tex_print(Tab, [[Rule, _], _, S]) :- 
         buss_tex_print_list(S, Tab),
    (Rule = ax -> % Check if the rule is Ax
            write('\\AxiomC{}\\RightLabel{$Ax.$}\n')
        ;
            write('\\RightLabel{$'),
            buss_tex_print_rule_name(Rule),
            write('$}')
    ),!,
    (buss_tex_is_branching(Rule) ->  % 
        write('\\BinaryInfC{$');
        write('\\UnaryInfC{$')),
    buss_tex_print_sequent(S),
    write('$}').
*/
buss_tex_name_variables(X, Z) :-
	buss_tex_name_variables(X, 0, _N, [], _Vs, Z).

buss_tex_name_variables(X, N, N, Vs, Vs, X) :- ground(X), !.
buss_tex_name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !.
buss_tex_name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !,
	V is N0 mod 3, VN is N0//3,
	buss_tex_name_var(V, VN, Z),
	N is N0+1.
buss_tex_name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !,
	buss_tex_name_variables(X, N0, N1, Vs0, Vs1, Z),
	buss_tex_name_variables(Xs, N1, N, Vs1, Vs, Zs).
buss_tex_name_variables(X, N0, N, Vs0, Vs, Z) :-
	X =.. Xs,
	buss_tex_name_variables(Xs, N0, N, Vs0, Vs, Zs),
	Z =.. Zs.

buss_tex_name_var(0, VN, X) :- !, buss_tex_name_var1([0'x], VN, X).
buss_tex_name_var(1, VN, X) :- !, buss_tex_name_var1([0'y], VN, X).
buss_tex_name_var(2, VN, X) :- !, buss_tex_name_var1([0'z], VN, X).

buss_tex_name_var1([V], 0, X) :- !, name(X, [V]).
buss_tex_name_var1([V], VN, X) :-
	name(VN, Ns), append(Ns, [0'}], Ns1),
	name(X, [V,0'_,0'{|Ns1]).

buss_tex_print_list([], _Tab).
buss_tex_print_list([S1], Tab) :- !,
	nl,
	Tab1 is Tab+2,
	buss_tex_print(Tab1, S1).
	%tabx(Tab).
buss_tex_print_list([S1|Ss], Tab) :- !,
	nl,
	Tab1 is Tab+2,
	buss_tex_print(Tab1, S1),
	%tabx(Tab1),
	buss_tex_print_list(Ss, Tab).

buss_tex_print_sequent((Xs-->Ys)) :-
	buss_tex_print_formulas(Xs),
	write(' \\fCenter '),
	buss_tex_print_formulas(Ys).

buss_tex_print_formulas([]).
buss_tex_print_formulas([A]) :- !,
	buss_tex_print_formula(A).
buss_tex_print_formulas([A|As]) :-
	buss_tex_print_formula(A),
	write(', '),
	buss_tex_print_formulas(As).

buss_tex_print_formula(A) :-
	buss_tex_print_formula(999, A).

buss_tex_print_formula(Prec0, A) :- buss_tex_quantifier_name(A, Q, X, B), !,
	Prec = 999,
	(Prec0 < Prec -> write('('); true),
	write(Q), write(' '), write(X), write('.'),
	buss_tex_print_formula(B),
	(Prec0 < Prec -> write(')'); true),
	!.
buss_tex_print_formula(Prec0, A) :- is_op(A, Prec, Type, Op, As), !,
	(Prec0 < Prec -> write('('); true),
	buss_tex_print_op_formula(Prec, Type, Op, As),
	(Prec0 < Prec -> write(')'); true),
	!.
buss_tex_print_formula(_Prec0, A) :- buss_tex_unit_name(A, U), !,
	write(U).
buss_tex_print_formula(_Prec0, A) :-
	rename_functor(A, A1),
	write(A1).

rename_functor(X, Z) :-
	X =.. [F0|As],
	capitalize_atom(F0, F),
	Z =.. [F|As].

buss_tex_quantifier_name(X@A, '\\forall', X, A).
buss_tex_quantifier_name(X#A, '\\exists', X, A).

buss_tex_unit_name(_, _) :- fail.
buss_tex_unit_name(bot, '\\bot').
buss_tex_unit_name(top, '\\top').

%buss_tex_print_op_formula(Prec, fy, Op, [A1]) :- Op = ~, !,
%	buss_tex_print_op(Op), write('{'),
%	buss_tex_print_formula(Prec, A1), write('}').
buss_tex_print_op_formula(Prec, fx, Op, [A1]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_op(Op), write(' '),
	buss_tex_print_formula(Prec1, A1).
buss_tex_print_op_formula(Prec, fy, Op, [A1]) :- !,
	buss_tex_print_op(Op), write(' '),
	buss_tex_print_formula(Prec, A1).
buss_tex_print_op_formula(Prec, xf, Op, [A1]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	write(' '), buss_tex_print_op(Op).
buss_tex_print_op_formula(Prec, yf, Op, [A1]) :- !,
	buss_tex_print_formula(Prec, A1),
	write(' '), buss_tex_print_op(Op).
buss_tex_print_op_formula(Prec, xfx, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	write(' '), buss_tex_print_op(Op), write(' '),
	buss_tex_print_formula(Prec1, A2).
buss_tex_print_op_formula(Prec, xfy, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec1, A1),
	write(' '), buss_tex_print_op(Op), write(' '),
	buss_tex_print_formula(Prec, A2).
buss_tex_print_op_formula(Prec, yfx, Op, [A1,A2]) :- !,
	Prec1 is Prec - 1,
	buss_tex_print_formula(Prec, A1),
	write(' '), buss_tex_print_op(Op), write(' '),
	buss_tex_print_formula(Prec1, A2).

is_op(A, Prec, Type, Op, As) :-
	functor(A, Op, N), current_op(Prec, Type, Op),
	is_op0(A, Type, N, As),
	!.
is_op0(A, fx, 1, [A1]) :- arg(1, A, A1).
is_op0(A, fy, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, yf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, xfy, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, yfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).

buss_tex_print_op(Op) :-
	buss_tex_op_name(Op, OpName), !,
	write(OpName).

buss_tex_op_name(~,  '\\lnot').
buss_tex_op_name(/\, '\\land').
buss_tex_op_name(\/, '\\lor').
buss_tex_op_name(->, '\\to').

buss_tex_print_rule_name([Rule,LN]) :- !,
	buss_tex_rule_name(Rule, RuleName),
	!,
	write(RuleName),
	write('('), write(LN), write(')').
buss_tex_print_rule_name(Rule) :-
	buss_tex_rule_name(Rule, RuleName),
	!,
	write(RuleName).

buss_tex_rule_name(ax, 'Ax').
buss_tex_rule_name(axiom, 'Axiom').
buss_tex_rule_name(l(top), 'L\\top').
buss_tex_rule_name(r(top), 'R\\top').
buss_tex_rule_name(l(bot), 'L\\bot').
buss_tex_rule_name(r(bot), 'R\\bot').
buss_tex_rule_name(l(~), 'L\\lnot').
buss_tex_rule_name(r(~), 'R\\lnot').
buss_tex_rule_name(l(/\), 'L\\land').
buss_tex_rule_name(r(/\), 'R\\land').
buss_tex_rule_name(l(\/), 'L\\lor').
buss_tex_rule_name(r(\/), 'R\\lor').
buss_tex_rule_name(l(->), 'L\\to').
buss_tex_rule_name(r(->), 'R\\to').
buss_tex_rule_name(l(all), 'L\\forall').
buss_tex_rule_name(r(all), 'R\\forall').
buss_tex_rule_name(l(exists), 'L\\exists').
buss_tex_rule_name(r(exists), 'R\\exists').
buss_tex_rule_name(cut, 'Cut').

buss_tex_is_branching(r(/\)).
buss_tex_is_branching(l(\/)).
buss_tex_is_branching(l(->)).

%%
%% End of bussproofs printer. 
%%
%%  Utilities
%%
append_all([], []).
append_all([P], P).
append_all([P|Ps], X) :- Ps=[_|_], append(P, X1, X), append_all(Ps, X1).

merge(X1, X2, X) :- split(X, X1, X2).

split([], [], []).
split([X|Xs], [X|Ys], Zs) :- split(Xs, Ys, Zs).
split([X|Xs], Ys, [X|Zs]) :- split(Xs, Ys, Zs).

append([], Z, Z).
append([W|X], Y, [W|Z]) :- append(X, Y, Z).

member(X, [X|_Xs]).
member(X, [_Y|Xs]) :- member(X, Xs).

memberq(X, [X|_Xs]) :- !.
memberq(X, [_Y|Xs]) :- memberq(X, Xs).

memq(X, [Y|_Xs]) :- X==Y, !.
memq(X, [_Y|Xs]) :- memq(X, Xs).

get_nth(0, [X|_Xs], X) :- !.
get_nth(N, [_|Xs], X) :- N>0, N1 is N-1, get_nth(N1, Xs, X).

for(I, M, N) :- M =< N, I=M.
for(I, M, N) :- M =< N, M1 is M+1, for(I, M1, N).

assoc(X, Z, [[X0|Z]|_As]) :- X==X0, !.
assoc(X, Z, [_|As]) :- assoc(X, Z, As).

substitute(X0, X, A0, A) :- var(A0), X0==A0, !, A=X.
substitute(_X0, _X, A0, A) :- var(A0), !, A=A0.
substitute(_X0, _X, A0, A) :- atomic(A0), !, A=A0.
substitute(X0, X, [A0|B0], [A|B]) :- !,
	substitute(X0, X, A0, A),
	substitute(X0, X, B0, B).
substitute(X0, X, A0, A) :-
	A0 =.. B0,
	substitute(X0, X, B0, B),
	A =.. B.

capitalize_atom(X, Z) :- atom(X),
	name(X, [C0|Cs]), C0 >= 0'a, C0 =< 0'z, !,
	C is ((C0 - 0'a) + 0'A),
	name(Z, [C|Cs]).
capitalize_atom(X, X).

n_write(0, _) :- !.
n_write(N, X) :- N>0, write(X), N1 is N-1, n_write(N1, X).

flush_out :-
	current_output(S),
	flush_output(S).
/*
goto_pos(T) :-
	current_output(S),
	line_position(S, T0),
	tabx(T-T0).

line_position(W) :-
	current_output(S),
	line_position(S, W).
*/
%%
%%  Logging
%%
log_start(yes) :- !,
	log_start('seqprover.log').
log_start(File) :-
	logging(no, _),
	!,
	open(File, write, STR),
	retractall(logging(_,_)),
	assert(logging(File, STR)).

log_end :-
	logging(no, _),
	!.
log_end :-
	logging(_File, STR),
	close(STR),
	fail.
log_end :-
	retractall(logging(_,_)),
	assert(logging(no, _)).

log_suspend(logging(File,STR)) :-
	logging(File, STR),
	retractall(logging(_,_)),
	assert(logging(no, _)).

log_resume(logging(File,STR)) :-
	retractall(logging(_,_)),
	assert(logging(File, STR)).

readx(STR, X) :-
	read(STR, X),
	echo_read(STR, X).

echo_read(user_input, _X) :-
	logging(no, _),
	!.
echo_read(user_input, X) :-
	logging(_File, STR),
	!,
	write(STR, X),
	write(STR, '.'),
	nl(STR).
echo_read(_, X) :-
	write(X),
	write('.'),
	nl.
/*
write(X) :-
	logging(no, _),
	!,
	write(X).

writey(X) :-
	logging(_, STR),
	write(X),
	write(STR, X).

nl :-
	logging(no, _),
	!,
	nl.
nl :-
	logging(_, STR),
	nl,
	nl(STR).

tabx(X) :-
	logging(no, _),
	!,
	tab(X).
tabx(X) :-
	logging(_, STR),
	tab(X),
	tab(STR, X).

%%
%%  Batch
%%
batch :-
	nl, write('# Start'), nl,
	% prolog_flag(syntax_errors, _, quiet),
	read(Output),
	read(Sequent),
	set_output_form(Output),
	batch_prove(Sequent),
	!,
	flush_out,
	halt.
batch :-
	nl, write('# Syntax error'), nl,
	flush_out,
	halt.

batch_prove((X <--> Y)) :- !,
	batch_prove((X --> Y)),
	nl,
	batch_prove((Y --> X)).
batch_prove(S0) :-
	(
	    convert_to_seq(S0, S),
	    sequentq(S)
	;
	    formulaq(S0),
	    S = ([] --> [S0])
	),
	!,
        write('# Proving '), write(S), nl,
	statistics(runtime, _),
	(prove(S, P) ->
	    statistics(runtime, [_,T]),
	    nl,
            write('# BEGIN Proof'), nl,
	    print_proof(P),
            nl, write('# END Proof'), nl,
	    nl, write('# Proved in '),
	    write(T), write(' msec.'), nl
	;
	    nl, write('# Fail to prove'), nl
	).
*/
%%
%%  Initialization
%%
:- seq_init.

This is an updated version that provides ‘Sequent-aligned’ proofs via bussproofs.sty, and this should be compatible with MathJax according to the documentation. Example:

Welcome to SWI-Prolog (threaded, 64 bits, version 9.0.4)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.
Please run ?- license. for legal details.

For online help and background, visit https://www.swi-prolog.org
For built-in help, use ?- help(Topic). or ?- apropos(Word).

?- true.

?- prover.
Sequent Calculus Prover ver 2.0 in Prolog
        by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cl(first)> X@f(X) -> Y@g(Y) <--> X#Y@(f(X) -> g(Y)).
_7972@f(_7972)->_7982@g(_7982)<-->_7972#_7982@(f(_7972)->g(_7982)).
Trying to prove with threshold =012
Succeed in proving  (58 msec.)
buss:1 =

\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}





\AxiomC{}\RightLabel{$Ax.$}
\UnaryInf$F(z) \fCenter F(z), G(x_{1}), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\to$}
\UnaryInf$ \fCenter F(z), F(z) \to G(x_{1}), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\forall$}
\UnaryInf$ \fCenter F(z), \forall y.F(z) \to G(y), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\exists$}
\UnaryInf$ \fCenter F(z), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\forall$}
\UnaryInf$ \fCenter \forall x.F(x), \exists x.\forall y.F(x) \to G(y)$




\AxiomC{}\RightLabel{$Ax.$}
\UnaryInf$F(y_{1}), G(z_{1}), \forall y.G(y) \fCenter G(z_{1}), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$L\forall$}
\UnaryInf$F(y_{1}), \forall y.G(y) \fCenter G(z_{1}), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\to$}
\UnaryInf$\forall y.G(y) \fCenter F(y_{1}) \to G(z_{1}), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\forall$}
\UnaryInf$\forall y.G(y) \fCenter \forall y.F(y_{1}) \to G(y), \exists x.\forall y.F(x) \to G(y)$\RightLabel{$R\exists$}
\UnaryInf$\forall y.G(y) \fCenter \exists x.\forall y.F(x) \to G(y)$\RightLabel{$L\to$}
\BinaryInf$(\forall x.F(x)) \to (\forall y.G(y)) \fCenter \exists x.\forall y.F(x) \to G(y)$
\end{prooftree}

Trying to prove with threshold =012
Succeed in proving  (12 msec.)
buss:2 =

\begin{prooftree}
\def\fCenter{\mbox{\ $\vdash$\ }}






\AxiomC{}\RightLabel{$Ax.$}
\UnaryInf$F(x_{1}), \forall x.F(x), \forall y.F(x_{1}) \to G(y) \fCenter F(x_{1}), G(z)$\RightLabel{$L\forall$}
\UnaryInf$\forall x.F(x), \forall y.F(x_{1}) \to G(y) \fCenter F(x_{1}), G(z)$
\AxiomC{}\RightLabel{$Ax.$}
\UnaryInf$\forall x.F(x), G(z), \forall y.F(x_{1}) \to G(y) \fCenter G(z)$\RightLabel{$L\to$}
\BinaryInf$\forall x.F(x), F(x_{1}) \to G(z), \forall y.F(x_{1}) \to G(y) \fCenter G(z)$\RightLabel{$L\forall$}
\UnaryInf$\forall x.F(x), \forall y.F(x_{1}) \to G(y) \fCenter G(z)$\RightLabel{$L\exists$}
\UnaryInf$\forall x.F(x), \exists x.\forall y.F(x) \to G(y) \fCenter G(z)$\RightLabel{$R\forall$}
\UnaryInf$\forall x.F(x), \exists x.\forall y.F(x) \to G(y) \fCenter \forall y.G(y)$\RightLabel{$R\to$}
\UnaryInf$\exists x.\forall y.F(x) \to G(y) \fCenter (\forall x.F(x)) \to (\forall y.G(y))$
\end{prooftree}

yes
cl(first)> 

The problem of spaces inside the proofs persists, and that Naoyuki Tamura in a discussion that I had with him is still present:

Le lun. 07/08/19 juil. 2019 à 12:13:27 , Naoyuki Tamura
<tamura@kobe-u.ac.jp> a envoyé ce message:
Dear Joseph,

I think you found a serious bug of seqprover.

For example, “X@p → p” can be proved, but “X@Y@p → p” cannot.
On the other hand, “all(X, all(Y, p)) → p” can be proved by
llprover.

So, there should be something wrong in the program of seqprover.

I don’t have a time to look at the code now, I will fix it in future.
Thanks again for your report.

– Naoyuki

I must say that Naoyuki was too generous with me. He saw the bug when I only reported a loop.

There is a little bitrot going on, links are broken now:

The link to “Examples 1. p\/p <--> p” here:
https://www.vidal-rosset.net/g4-prover/

Shows just a blank page.

And the link to “Sequent Prover (seqprover)” here:
https://www.vidal-rosset.net/g4-prover/

Shows just your home page.

Thanks. I know this problem created by updating the server, and I do not succeed to solve it.

(Nothing of Importance)