Premises: click the first line and type (letters become capitals), or use the symbol buttons. Enter adds another premise below.

Tree: hover over or click a line to show its two small buttons. The vertical-line button adds a line joined by a conjunction; the V-shaped button splits into two branches (disjunction). From the first conjunction or disjunction on, new lines belong to the tree.

NegConclusion: negates the last premise in place (a leading ⊢ is dropped) and adds “NegConc” behind the line. No line is added, because a negated line next to the conclusion would close the tree at once. If that line is already negated over its whole length, the negation disappears instead.

Negation: select letters or symbols in a line. Negate draws a line over the selection (below a longer negation, or above a negation already inside the selection); Merge joins separate negations under one line; Remove takes off the top line. Two lines at most — only the buttons that make sense for the selection are active.

Step number: adds a number of your choice (1–99) with a check mark at the end of the current line, to show at which step it was worked out.

Close and Open: Close (×) marks a contradictory branch; Open (⋮) marks a branch that stays open. Either way nothing more can be added under the line (Undo to go back).

Undo goes back (up to 5 steps) and Clear starts a new tree. Enlarge opens the editor bigger; Copy as image and Export to Word let you reuse the tree elsewhere.