Kripke Model

Testing and quality assurance are very time-consuming stages of the software development process. Various techniques are used to reduce the cost and time these stages consume. One such technique is software verification. Model checking is an approach to software verification based on Kripke models.

A Kripke model is a 5-tuple $(P, S, S_0, R, L)$, where $P$ is a finite set of atomic propositions, $S$ is a finite set of states, $S_0 \subset S$ is a set of initial states, $R \subset S \times S$ is a transition relation, and $L \subset S \times P$ is a truth relation. In this problem we ignore initial states, and $R$ is reflexive, so $R(s, s)$ holds for every state $s \in S$.

A path $\pi$ beginning in state $s$ is an infinite sequence of states $s_0 s_1 \ldots$ such that $s_0 = s$ and $(s_i, s_{i+1}) \in R$ for every $i \ge 0$.

Temporal logic and its subset Computation Tree Logic (CTL) describe propositions qualified in terms of time. Kripke models are often used to check properties described in CTL.

There are two kinds of CTL formulae: state formulae and path formulae, evaluated over states and paths respectively.

If $p \in P$, then $p$ is a state formula that holds in state $s$ iff $(s, p) \in L$.

If $f$ is a path formula, then $\mathrm{\mathbf{A}} f$ and $\mathrm{\mathbf{E}} f$ are state formulae, where $\mathrm{\mathbf{A}}$ and $\mathrm{\mathbf{E}}$ are path quantifiers:

• $\mathrm{\mathbf{A}} f$ holds in state $s$ iff $f$ holds for every path beginning in $s$;
• $\mathrm{\mathbf{E}} f$ holds in state $s$ iff there exists a path $\pi$ beginning in $s$ for which $f$ holds.

If $f$ and $g$ are state formulae, then $\mathrm{\mathbf{G}} f$ and $f \mathrm{\mathbf{U}} g$ are path formulae, where $\mathrm{\mathbf{G}}$ and $\mathrm{\mathbf{U}}$ are temporal operators:

• $\mathrm{\mathbf{G}} f$ (Globally) holds for a path $\pi = s_0 s_1 \ldots$ iff $f$ holds in state $s_i$ for every $i \ge 0$;
• $f \mathrm{\mathbf{U}} g$ (Until) holds for a path $\pi = s_0 s_1 \ldots$ iff there exists $i \ge 0$ such that $g$ holds in state $s_i$ and $f$ holds in every state $s_0, s_1, \ldots, s_{i-1}$.

To verify a property described by a state formula $f$ means to find every state in which $f$ holds. Verifying an arbitrary property is quite complex. Your task is easier: write a program that verifies the property described by the temporal-logic formula $\mathrm{\mathbf{E}}(x \mathrm{\mathbf{U}} (\mathrm{\mathbf{A}} \mathrm{\mathbf{G}} y))$, where $x$ and $y$ are atomic propositions.

The first line contains three positive integers $n$, $m$, and $k$ — the number of states, transitions, and atomic propositions ($1 \le n \le 10\,000$; $0 \le m \le 100\,000$; $1 \le k \le 26$).

Each of the next $n$ lines describes one state. State $i$ ($1 \le i \le n$) is described by $c_i$ — the number of atomic propositions that are true in this state — followed by a space-separated list of those propositions ($0 \le c_i \le k$). Atomic propositions are denoted by the first $k$ lowercase English letters.

Each of the next $m$ lines describes one transition and contains two integers $s$ and $t$ ($1 \le s, t \le n$; $s \ne t$) — a transition from state $s$ to state $t$. The model also contains an implicit self-loop $(s, s)$ for every state $s$ (these are not listed in the input). No transition is listed twice.

The last line contains the property to verify, always of the form E(xU(AGy)), where x and y are atomic propositions.

On the first line, print the number of states in which the verified property holds. On the following lines, print the numbers of those states in increasing order.