Residuated Lattice Inequations Quiz

The randomly generated (in)equations below are in the language of (bounded) residuated lattices. Specifically, the language used here has Recall that a residuated lattice is of the form where is a lattice, is a monoid, and for all T is the top element of the lattice, 0 is the bottom element, and 1 is the unit with respect to the monoid operation *.

Decide if the following inequations are true in the theory of bounded residuated lattices.

Click here to

Click here to get a
The algorithm implemented here is due to Okada and Terui, JSL 64(2), 1999. A version of this algorithm for residuated lattices is described in the preprint A Gentzen systems and decidability for residuated lattices (P. Jipsen, Jan 2000) pdf version