Result of llprover

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

                      ------- Ax
                      b --> b
------- Ax            ---------- L/\2       ------- Ax
a --> a               a/\b --> b            c --> c
---------- L/\1       --------------- L/\1  --------------- L/\2
a/\b --> a            (a/\b)/\c --> b       (a/\b)/\c --> c
--------------- L/\1  ------------------------------------- R/\
(a/\b)/\c --> a                (a/\b)/\c --> b/\c
------------------------------------------------- R/\
              (a/\b)/\c --> a/\b/\c

CPU Time = 0 msec.

                    ------- Ax
                    b --> b
------- Ax          ---------- L/\1     ------- Ax
a --> a             b/\c --> b          c --> c
------------- L/\1  ------------- L/\2  ---------- L/\2
a/\b/\c --> a       a/\b/\c --> b       b/\c --> c
--------------------------------- R/\   ------------- L/\2
        a/\b/\c --> a/\b                a/\b/\c --> c
        --------------------------------------------- R/\
                    a/\b/\c --> (a/\b)/\c

CPU Time = 0 msec.


Naoyuki Tamura