9128: Reasoning

    The reasoning system consists of the following symbols:
    1. Parentheses: ( and );
    2. Logical connectives: ¬ and →;
    3. Universal quantifier: ∀;
    4. Variables: u − z;
    5. Constants: a − e;
    6. Functions: f − h;
    7. 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:
    1. Every variable v is a term.
    2. Every constant c is a term.
    3. If t₁, . . . , t_n are terms and f is a function, then f t₁ . . . t_n is a term.
    Formula (well-formed formula) is defined as follows:
    1. If t₁, . . . , t_n are terms and P is a predicate, then P t₁ . . . t_n is a formula. This kind of formula is also called the atomic formula.
    2. If φ and ψ are formulas, then (¬φ) and (φ → ψ) are both formulas.
    3. If φ is a formula, and v is a variable, then ∀vφ is also a formula.
    Free occurrence of a variable x in formula φ is defined as follows:
    1. If φ is an atomic formula, then x occurs free in φ if and only if x occurs in φ (which means there is a char x inside the string φ).
    2. If φ is (¬ψ), then x occurs free in φ if and only if x occurs free in ψ.
    3. If φ is (ψ → γ), then x occurs free in φ if and only if x occurs free in ψ or x occurs free in γ.
    4. If φ is ∀vψ, then x occurs free in φ if and only if x occurs free in ψ and x ̸= v.
    For every formula φ, every variable x, and every term t, the replacement φ x t is defined as:
    1. If φ is an atomic formula, then φxt is the expression formed by simply replacing every char x to string t.
    2. If φ is ¬ψ, then (¬ψ)xt = (¬ψtx).
    3. If φ is ψ → γ, then (ψ → γ)xt = (ψtx → γtx)
    4. If φ is ∀yψ, then (∀yψ) xt =    ∀y(ψtx), if x ̸= y  or  ∀yψ, if x = y.
    And finally, we can now define the rule of zero-contradiction replacement:
    1. For atomic formula φ, t can always replace x in φ without contradiction.
    2. If φ is ¬ψ, then t can replace x in φ without contradiction if and only if t can replace x without contradiction in ψ.
    3. If φ is ψ → γ, then t can replace x in φ without contradiction if and only if t can replace x without contradiction in both ψ and γ.
    4. If φ is ∀yψ, then t can replace x in φ without contradiction if and only if
        (a) x doesn’t occur free in φ, or
        (b) y doesn’t occur in t, and t can replace x in ψ 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 ≤ T ≤ 10), indicating the number of test cases.
    For every test case, the first line gives a formula A, which has length L(1 ≤ L ≤ 100). In the input formula, ¬ will be replaced by char N, → will be replaced by char I, and ∀ 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 ≤ q ≤ 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.

    The given formula is ∀x∀y(P(z, v, f(x, y, g(x, y))) → (¬Q)).
    For the first and the second query, x and y don't occur free in the formula, because they are constrained by ∀. Thus the answer is the original formula.
    For the third query, z occurs free in the formula, because it isn't constrained by ∀. 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 ∀x, making the x in h(x, z) no longer occur free. Thus the replacement is illegal.