# 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,r     p,r --> p,r      p,r --> q,r     p,r,r --> r      q --> q,p,r     q,r --> p,r      q,r --> q,r     q,r,r --> r
--------------------------- L->  --------------------------- L->  --------------------------- L->  --------------------------- L->
p,q->r --> p,r                   p,r,q->r --> r                   q,q->r --> p,r                   q,r,q->r --> r
----------------------------------------------- L->               ----------------------------------------------- L->
p,p->r,q->r --> r                                                 q,p->r,q->r --> r
----------------------------------------------------------------------------------- L\/
p\/q,p->r,q->r --> r
--------------------- R->
p->r,q->r --> p\/q->r
-------------------------- L/\
(p->r)/\(q->r) --> p\/q->r

# Proved in 0 msec.

Trying to prove with threshold = 0

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

# Proved in 0 msec.
```

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura