Sequent Prover (seqprover)

Sequent:
Output style:

[Top page]


Trying to prove with threshold = 0

----------- Ax  ----------- Ax   ----------- Ax  ----------- Ax
p --> q,p,r     p,r --> p,r      p,q --> q,r     p,q,r --> r
--------------------------- L->  --------------------------- L->
      p,q->r --> p,r                   p,q,q->r --> r
      ----------------------------------------------- L->
                     p,p->q,q->r --> r
                     ------------------ R->
                     p->q,q->r --> p->r

# Proved in 0 msec.

Maintained by Naoyuki Tamura / Programmed by Naoyuki Tamura