Result of llprover

You are the 129742-nd user of this script.
System:
Sequent:
Output Style:
Threshold value:

            ------- Ax  ------- Ax
            b --> b     c --> c
------- Ax  ------------------- L->
a --> a        b,b->c --> c
--------------------------- L->
     a,b,a->b->c --> c
     ----------------- L*
     a*b,a->b->c --> c
     ------------------ R->
     a->b->c --> a*b->c

CPU Time = 0 msec.

------- Ax  ------- Ax
a --> a     b --> b
------------------- R*  ------- Ax
    b,a --> a*b         c --> c
    --------------------------- L->
         b,a,a*b->c --> c
         ----------------- R->
         a,a*b->c --> b->c
         ------------------ R->
         a*b->c --> a->b->c

CPU Time = 0 msec.


Naoyuki Tamura