The algorithm implemented here 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.
With a simple translation, the same algorithm can be used to decide the equational theory of the variety of negative cones of l-groups.
Recently N. Galatos discovered a further translation that gives a decision procedure for integral generalized MV-algebras. He also shows that an equation holds for all generalized MV-algebras iff it holds for integral generalized MV-algebras and for l-groups.
The (in)equations are in the language of l-groups (or 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.)
Test yourself by deciding randomly generated l-group equations.
The JavaScript code is available for browsing.