The algorithm implemented here uses a translation, due to N. Galatos (see his forthcoming dissertation), to the decision procedure for lattice-ordered groups. The algorithm for deciding equations in l-groups is due to W. C. Holland and S. H. McCleary, Solvability of the word problem in free lattice-ordered groups, Houston Journal of mathematics, 5(1), (1979) p. 99--105.
The (in)equations are in the language of residuated lattices. Specifically, the language used here has
Enter your own (in)equation and check if it holds in the varieties LG, LG-, IGMV, and GMV. (An (in)equation holds in GMV iff it holds in LG and IGMV.)