The right hand-side of a rule

You can draw/complete the graph of the right hand-side of a rule. It corresponds to element that will be added to your model in construction during the execution of the tableau method.

Any extra variables (in upper-case) are instanciated with new symbols. For instance variable S will be instanciated in a new symbol s1, s2, s3... variable PHI will be instanciated in a new symbol p1, p2, p3...

If you want to compute something you need to "unquote" your expression by using a comma. For instance, ,(+ 'N 1) will add the successor of the number N (if N denotes a number!).