Opens a supplementary window in which program execution can be seen in progress. The main branch of the proof tree under construction for the goal being processed is displayed. The subgoals that have already been successfully satisfied appear in blue or in green . Those but partly satisfied (which are satisfying at the moment) appear in red, and the ones not yet reached appear in black.

Information in this window duplicates that in Stack window and other trace windows but it is easier to interpret.

You can change the mode of the Proof Tree window by the buttons: N, S, T, U, H, P, V.

N – show stack numbers
S – short print
T – tight print
U – underline
H – highlight
P – prefix view
V – show variables

You can click on atoms to select them. You can copy in the clipboard the selected atom with the Ctrl button. After that you can paste it by Ctrl+V in your program.

You can double click on blue atoms to see how they are satisfied. Note that the terms that instantiate variables in these branches can be seen too. If you double click a subgoal and hear sound beep, this means that this subgoal is instantiated with an axiom. If you want to receive the normal view of the Proof Tree again then double click on the last red subgoal. If you double click on a green subgoal then you will close its subtree.

You can use buttons Home, End and Insert for horizontal scrolling of this window.

Home scrolls to the beginning (the most left point).
End scrolls to the end (the most right point).
Insert scrolls to the middle.

Use also Page Up , Page Down and arrows .

Warning: The numbers of the variables in the subgoals which are in black may be not real in some sense. The reason: If this number is bigger than the maximum in the Variables window, then this is a not-instantiated variable with temporal number. The numbers of other variables are real and they are shown in the Variables window. Of course, these numbers are real but not constant because after backtracking they can change.