Legend:
Variable names start with a small latin letter and can contain small latin letters and numbers.
Names starting with a small letter 'c' are considered nominals.
#   - [0] - Necessity
@   - <0> - Possibility
#'  - [0]-1 - Reversed Necessity
@'  - <0>-1 - Reversed Possibility
[U] - Universal necessity
<U> - Universal possibility
[n] - Necessity with relation index, where n is a number
<n> - Possibility with relation index, where n is a number
[n]'- Reversed Necessity with relation index, where n is a number
<n>'- Reversed Possibility with relation index, where n is a number
&   - And - Conjunction
|   - Or - Disjunction
~   - Not - Negation
->  - Implication
<-  - Reversed Implication
<-> - Equivalence