# Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]

```Trying to prove with threshold = 0

----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax
p,q --> p,p     p,r --> p,p      p,q --> p,r     p,r --> p,r      p,q --> q,p     p,r --> q,p      p,q --> q,r     p,r --> q,r
--------------------------- L\/  --------------------------- L\/  --------------------------- L\/  --------------------------- L\/
p,q\/r --> p,p                   p,q\/r --> p,r                   p,q\/r --> q,p                   p,q\/r --> q,r
----------------------------------------------- R/\               ----------------------------------------------- R/\
p,q\/r --> p,p/\r                                                 p,q\/r --> q,p/\r
----------------------------------------------------------------------------------- R/\
p,q\/r --> p/\q,p/\r
----------------------- R\/
p,q\/r --> (p/\q)\/p/\r
------------------------ L/\
p/\q\/r --> (p/\q)\/p/\r

# Proved in 0 msec.

Trying to prove with threshold = 0

----------- Ax    ----------- Ax
p,q --> q,r       p,r --> q,r
--------- Ax    --------- Ax    ------------ L/\  ------------ L/\
p,q --> p       p,r --> p       p/\q --> q,r      p/\r --> q,r
---------- L/\  ---------- L/\  ------------------------------ L\/
p/\q --> p      p/\r --> p           (p/\q)\/p/\r --> q,r
-------------------------- L\/       --------------------- R\/
(p/\q)\/p/\r --> p               (p/\q)\/p/\r --> q\/r
------------------------------------------------------ R/\
(p/\q)\/p/\r --> p/\q\/r

# Proved in 0 msec.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura