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).

Check rules: after applying rules, click “Check rules”. Give every decomposed formula a step number: the checker verifies that its results appear on every open branch in the right shape (two lines one under the other for a conjunctive rule, a split for a disjunctive rule), that every line or split comes from a rule applied higher up, that every × is justified by a formula and its negation, that a branch marked ⋮ is really complete and free of contradiction, that the conjunctive rules were applied before the disjunctive ones, and that the step numbers run 1, 2, 3… (no repeats or gaps, in the order the rules were applied, from the top of the tree down). Lines are coloured: green = rule correct, red = error, orange = remark or still to do. Click a message to jump to its line.

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.