###
A brief explanation of the output

Each line of a proof consists of a list of RL terms, the sequent turnstile !-, another
RL term, and finally the name of a rule that was applied to derive this line.
There are left and right rules for each of the operation symbols in the language
of residuated lattices. Gentzen system rules are usually written in a positive
style, with a list of premises above a horizontal line, followed by the conclusion below.
When searching for a proof, such rules are applied from bottom to top, producing
trees that grow upwards, and expand in width very rapidly. Such proofs are not
easily displayed on a webpage, so here we use a different approach based on the
Fitch style of presenting natural deduction proofs.
(Reformated rules to be inserted here...)

To display the proofs in a linear fashion, rather than the more usual Gentzen style,
the proof trees are displayed from the root downwards, with the depth of nodes indicated
by the indentation level. (Only the branching rules increase the indentation depth.)
Each sequent is labeled by the name of the rule that produced it. When a terminal
node is reached, the indentation level decreases again. With a bit of practice, these
proofs are actually easier to read (and write) than the standard tree-like presentation.
The symbol !- can be interpreted as *not less or equal*, in which case
each line implies the one below it (if at the same indentation level) or one
of the two indented alternatives (in the case of a branching rule). With this
interpretation, the terminal nodes represent contradictions, reminiscent of
a tableau style proof.