{ satisfiable } conj (<>p1, <>(p1 & <>p1), [] conj (p1, <>p1, <>(<>-p1 & []p2)), []-p2, (p1 <-> p3), [](p1 <-> p3), disj (p11, p12, p13, p14, p15), disj (-p11, -p12, -p13), [][][](p11 <-> p12))