Under construction

Still being built. Things may change

Testing Logical Equation Identities

Time limit8sMemory limit512 MB

Summary
Parse two logical formulas and decide whether they take the same truth value for every assignment of the variables a through k.
Level

Easy3 of 10

Topics
String, Brute force, Recursion, Implementation
Solved
No attempts yet

Problem

Logical operations handle only two values, T and F.

"-" is a unary operator (a symbol for an operation with one input), and "*", "+", and "->" are binary operators (symbols for operations with two inputs). "-" is logical negation (NOT), "*" is logical conjunction (AND), "+" is logical disjunction (OR), and "->" is logical implication (IMP). The truth tables for these logical operations are shown below.

xy-x(x*y)(x+y)(x->y)
TTFTTT
TFFFTF
FTTFTT
FFTFFT

A logical formula has one of the following forms. X and Y are logical formulas, and a binary operator is always enclosed in parentheses.

  • Constant: T, F
  • Variable: a, b, c, d, e, f, g, h, i, j, k
  • Logical negation: -X
  • Logical conjunction: (X*Y)
  • Logical disjunction: (X+Y)
  • Logical implication: (X->Y)

You are given an equation formed by joining two logical formulas with an equals sign "=". An identity is an equation that holds no matter what values the variables appearing in it take. We want to write a program that determines whether a given equation is an identity.

Input

The input consists of multiple lines, each of which is one dataset. A dataset is a string made of T, F, a, b, c, d, e, f, g, h, i, j, k, (, ), =, -, +, *, >, and contains no other characters such as spaces. You may assume that each line is at most 1000 characters long.

One dataset contains one equation. The grammar of an equation is given by the following BNF. Every equation follows these syntax rules.

<equation> ::= <formula> "=" <formula>
<formula>  ::= "T" | "F" |
"a" | "b" | "c" | "d" | "e" | "f" |
"g" | "h" | "i" | "j" | "k" |
"-" <formula> |
"(" <formula> "*" <formula> ")" |
"(" <formula> "+" <formula> ")" |
"(" <formula> "->" <formula> ")"

The end of the input is indicated by a line consisting of only "#", and this line is not a dataset.

Output

For each dataset, output "YES" on its own line if the equation is an identity, and "NO" otherwise. The output must not contain extra characters.

Examples1

  1. Example 1

    Input
    -(a+b)=(-a*-b)
(a->b)=(-a+b)
((a*T)+b)=(-c+(a*-b))
#
    Expected output
    YES
YES
NO