Reasoning

The reasoning system consists of the following symbols:

- Parentheses: $($ and $)$;
- Logical connectives: $\neg$ and $\to$;
- Universal quantifier: $\forall$;
- Variables: $u-z$;
- Constants: $a-e$;
- Functions: $f-h$;
- Predicates: $P-T$.

This reasoning system also includes concepts such as term, formula, free occurrence, and replacement. Based on these concepts, we can define whether a certain term $t$ can replace a certain variable $x$ without contradiction. This is one of the basis for reasoning, and you wants to solve this problem first.

Term is defined as follows:

- Every variable $v$ is a term.
- Every constant $c$ is a term.
- If $t_1,\dots,t_n$ are terms and $f$ is a function, then $ft_1\dots t_n$ is a term.

Formula (well-formed formula) is defined as follows:

- If $t_1,\dots,t_n$ are terms and $P$ is a predicate, then $Pt_1\dots t_n$ is a formula. This kind of formula is also called the atomic formula.
- If $\varphi$ and $\psi$ are formulas, then $(\neg\varphi)$ and $(\varphi\to\psi)$ are both formulas.
- If $\varphi$ is a formula, and $v$ is a variable, then $\forall v\varphi$ is also a formula.

Free occurrence of a variable $x$ in formula $\varphi$ is defined as follows:

- If $\varphi$ is an atomic formula, then $x$ occurs free in $\varphi$ if and only if $x$ occurs in $\varphi$ (which means there is a char $x$ inside the string $\varphi$).
- If $\varphi$ is $(\neg\psi)$, then $x$ occurs free in $\varphi$ if and only if $x$ occurs free in $\psi$.
- If $\varphi$ is $(\psi\to\gamma)$, then $x$ occurs free in $\varphi$ if and only if $x$ occurs free in $\psi$ or $x$ occurs free in $\gamma$.
- If $\varphi$ is $\forall v\psi$, then $x$ occurs free in $\varphi$ if and only if $x$ occurs free in $\psi$ and $x\ne v$.

For every formula $\varphi$, every variable $x$, and every term $t$, the replacement $\varphi_t^x$ is defined as:

- If $\varphi$ is an atomic formula, then $\varphi_t^x$ is the expression formed by simply replacing every char $x$ to string $t$.
- If $\varphi$ is $(\neg\psi)$, then $(\neg\psi)^x_t=(\neg\psi^x_t)$.
- If $\varphi$ is $(\psi\to\gamma)$, then $(\psi\to\gamma)^x_t=(\psi^x_t\to\gamma^x_t)$
- If $\varphi$ is $\forall y\psi$, then $(\forall y\psi)^x_t=
\begin{cases}
\forall y(\psi^x_t),&\text{if } x\ne y;\\\\
\forall y\psi,&\text{if } x=y.
\end{cases}$

And finally, we can now define the rule of zero-contradiction replacement:

- For atomic formula $\varphi$, $t$ can always replace $x$ in $\varphi$ without contradiction.

- If $\varphi$ is $(\neg\psi)$, then $t$ can replace $x$ in $\varphi$ without contradiction if and only if $t$ can replace $x$ without contradiction in $\psi$.

- If $\varphi$ is $(\psi\to\gamma)$, then $t$ can replace $x$ in $\varphi$ without contradiction if and only if $t$ can replace $x$ without contradiction in both $\psi$ and $\gamma$.

- If $\varphi$ is $\forall y\psi$, then $t$ can replace $x$ in $\varphi$ without contradiction if and only if

1. $x$ doesn't occur free in $\varphi$, or

2. $y$ doesn't occur in $t$, and $t$ can replace $x$ in $\psi$ without contradiction.

Now, by programming, Jack wants to judge whether $x$ is replaceable by the term $t$ without contradiction.

At the beginning of the input section, there is an integer $T(1\le T\le 10)$, indicating the number of test cases.

For every test case, the first line gives a formula $A$, which has length $L(1\le L\le 100)$.
In the input formula, $\neg$ will be replaced by char $N$, $\to$ will be replaced by char $I$, and $\forall$ will be replaced by char $A$.

The next line consists of an integer $m$, denoting the number of function and predicate.

Then there followed $m$ lines, each line consists of a char and an integer, representing the parameter number of the function or predicate.

The next line consists of an integer $q(1\le q\le 100)$, denoting $q$ queries.

There follow $q$ lines, each of which consists of a term $t$ and a variable $x$, denoting the query of whether the term $t$ can replace the variable $x$ in the formula A without replacement. It is guaranteed that the length of string $t$ is no more than $100$.

The output consists of $q$ sections.

In each section, you need to print a character $Y/N$ to answer whether the variable is replaceable without contradiction.

If the answer is yes, you should print the formula $A'$ after replacement.

1
AxAy(PzvfxygxyI(NQ))
5
f 3
g 2
P 3
Q 0
h 2
4
hxx x
hxy y
hzz z
hxz z

Y
AxAy(PzvfxygxyI(NQ))
Y
AxAy(PzvfxygxyI(NQ))
Y
AxAy(PhzzvfxygxyI(NQ))
N

The given formula is $\forall x\forall y(P(z, v, f(x, y, g(x, y)))\to(\neg Q))$.

For the first and the second query, $x$ and $y$ don't occur free in the formula, because they are constrained by $\forall$. Thus the answer is the original formula.

For the third query, $z$ occurs free in the formula, because it isn't constrained by $\forall$. Thus the answer is to replace $z$ by $h(z, z)$.

For the last query, $z$ occurs free in the formula, and after the replacement, $x$ in $h(x, z)$ will be constrained by $\forall x$, making the $x$ in $h(x, z)$ no longer occur free. Thus the replacement is illegal.

2023“钉耙编程”中国大学生算法设计超级联赛（9）