<none yet>

The tree format is defined as follows.

• The tree as a whole is module-qualified with the same module as the input Stack.
• Each node takes the shape Node-Children, where Node is an atom (in the logical sense) and Children is a (possibly empty) list of sub-trees that justify the Node.
• Nodes (atom) may be wrapped in one or more of

  not(Node)

  NAF negation

  - Node

  Classical negation

  chs(Node)

  Node was proven by co-induction ("it is assumed that ...")

  proved(Node)

  Node was proven before ("justified above")

  assume(Node)

  Node was assumed (matching chs(Node)).

The root node has the atom query and has two children: the actual query and the atom o_nmr_check which represents the global constraints.