```    G4 Prover
Result of the test for sequent p\/(q\/r) <--> (p\/q)\/r

G4 Prover: a Prolog Prover for Roy Dyckhoff's Sequent Calculus G4
This prover is a fork made by Joseph Vidal-Rosset (joseph.vidal-rosset@gmail.com),
from seqprover.pl, the sequent prover for CL-X, written by Naoyuki Tamura (tamura@kobe-u.ac.jp).
Type "help." if you need some help.
fol(g4i)> fol(g4i).
yes
fol(g4i)> output(pretty).
yes
fol(g4i)> p\/q\/r<-->(p\/q)\/r.
Trying to prove with threshold = 0
Succeed in proving p\/q\/r --> (p\/q)\/r (5 msec.)
pretty:1 =
------- Ax
q --> q
------- Ax           ---------- R\/       ------- Ax
p --> p              q --> p\/q           r --> r
---------- R\/       --------------- R\/  --------------- R\/
p --> p\/q           q --> (p\/q)\/r      r --> (p\/q)\/r
--------------- R\/  ------------------------------------ L\/
p --> (p\/q)\/r               q\/r --> (p\/q)\/r
------------------------------------------------ L\/
p\/q\/r --> (p\/q)\/r
Trying to prove with threshold = 0
Succeed in proving (p\/q)\/r --> p\/q\/r (4 msec.)
pretty:2 =
------- Ax
q --> q
------- Ax         ---------- R\/     ------- Ax
p --> p            q --> q\/r         r --> r
------------- R\/  ------------- R\/  ---------- R\/
p --> p\/q\/r      q --> p\/q\/r      r --> q\/r
-------------------------------- L\/  ------------- R\/
p\/q --> p\/q\/r              r --> p\/q\/r
------------------------------------------- L\/
(p\/q)\/r --> p\/q\/r
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 13 msec.
true

Back to g4-prover
Maintained by  Joseph Vidal-Rosset
```