```    G4 Prover
Result of the test for sequent p\/(q/\r) <--> (p\/q)/\(p\/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)/\p\/r.
Trying to prove with threshold = 0
Succeed in proving p\/q/\r --> (p\/q)/\p\/r (5 msec.)
pretty:1 =
--------- Ax      --------- Ax
q,r --> q         q,r --> r
------- Ax      ------- Ax      ------------ R\/  ------------ R\/
p --> p         p --> p         q,r --> p\/q      q,r --> p\/r
---------- R\/  ---------- R\/  ------------------------------ R/\
p --> p\/q      p --> p\/r           q,r --> (p\/q)/\p\/r
-------------------------- R/\       --------------------- L/\
p --> (p\/q)/\p\/r               q/\r --> (p\/q)/\p\/r
------------------------------------------------------ L\/
p\/q/\r --> (p\/q)/\p\/r
Trying to prove with threshold = 0
Succeed in proving (p\/q)/\p\/r --> p\/q/\r (5 msec.)
pretty:2 =
--------- Ax  --------- Ax
q,r --> q     q,r --> r
--------- Ax         --------- Ax         --------- Ax    ----------------------- R/\
p,p --> p            p,r --> p            q,p --> p            q,r --> q/\r
--------------- R\/  --------------- R\/  --------------- R\/  --------------- R\/
p,p --> p\/q/\r      p,r --> p\/q/\r      q,p --> p\/q/\r      q,r --> p\/q/\r
------------------------------------ L\/  ------------------------------------ L\/
p,p\/r --> p\/q/\r                        q,p\/r --> p\/q/\r
------------------------------------------------------------ L\/
p\/q,p\/r --> p\/q/\r
------------------------ L/\
(p\/q)/\p\/r --> p\/q/\r
yes
fol(g4i)> quit.
yes
Exit from Sequent Calculus Prover...
Total CPU time = 16 msec.
true

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