Current: ([0]([0]Not p Or p Or q) And [0]([0]Not p Or Not p Or Not q))

Nominal Formula: ((Not (C1 -> <0>C2) Or Not (C2 -> <0>C3) Or (C2 And C3)) And (C1 And [0][0]0))

First-Order Formula: For-All y1 For-All y2(((y1 = y2) Or Not (xRy1) Or Not (y1Ry2)) And For-All z1((xRz1) -> For-All z2Not (z1Rz2)))

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.
#   - necessity.png - Necessity
@   - possibility.png - Possibility
#'  - necessity.png-1 - Reversed Necessity
@'  - possibility.png-1 - Reversed 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.png - Conjunction
|   - or.png - Disjunction
~   - not.png - Negation
->  - Implication
<-  - Reversed Implication
<-> - Equivalence