=> stop clear stages[n] width[n] cut[n]

=> is a button for starting a proof search (same as run menu item)

stop is button for stopping the search

clear is button for clearing the tabs [tree,console,aux,???]

stages[n] is a button (control on/off) and a number selector.
When the stages button is clicked ON it shows color stages. The selector chooses how many inference stages to allow before stoping the search. When this control is off, there is no limit on the number of inference stages.

width[n] is a button (control on/off) and a number selector.
When the width button is clicked ON it shows color width. The selector chooses how many branches (tree width) to allow. When this control is off, there is no limit on the growth of new search branches.

cut[n] is a button (control on/off) and a number selector.
When the cut button is clicked ON it shows color cut. The selector chooses how much additional complexity a rule is allowed to introduce into a consequent literal over and above the maximum complexity of an antecedent literal. Similarly, regarding modulators: how much more complex the Rterm of a rewrite can exceed that of the term. The complexity of a term is the maximum number of nested operators in any subterm. When this control is off, there is no limit on the growth of term complexity caused by rules or equality modulators.