Current: ((<0>[0](p Or q Or r) And <0>[0](p Or q Or Not r) And <0>[0](p Or r Or Not q) And <0>[0](p Or Not q Or Not r) And <0>[0](q Or r Or Not p) And <0>[0](q Or Not p Or Not r) And <0>[0](r Or Not p Or Not q) And <0>[0](Not p Or Not q Or Not r)) -> 0)

Nominal Formula: (Not (C1 -> <0>C2) Or Not (C1 -> <0>C3) Or Not (C1 -> <0>C4) Or Not (C1 -> <0>C5) Or Not (C1 -> <0>C6) Or Not (C1 -> <0>C7) Or Not (C1 -> <0>C8) Or (C1 And [0]<0>(<0>-1C2 And <0>-1C3 And <0>-1C4 And <0>-1C5 And <0>-1C6 And <0>-1C7 And <0>-1C8)))

First-Order Formula: For-All y1 For-All y2 For-All y3 For-All y4 For-All y5 For-All y6 For-All y7(Not (xRy1) Or Not (xRy2) Or Not (xRy3) Or Not (xRy4) Or Not (xRy5) Or Not (xRy6) Or Not (xRy7) Or For-All z1((xRz1) -> Exists z2((z1Rz2) And (y1Rz2) And (y2Rz2) And (y3Rz2) And (y4Rz2) And (y5Rz2) And (y6Rz2) And (y7Rz2))))

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