Reasoning

Problem Description

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.

Input

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$.

Output

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.

Sample Input

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

Sample Output

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

Hint

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.

Source

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