함의

명제 논리에서 쓰는 연결사가 함의와 부정 두 가지뿐인 체계를 다룬다. 가정으로 주어진 논리식이 모두 참이라고 할 때, 질의로 주어진 논리식 각각이 항상 참인지 판정한다.

함의 A->B는 앞이 참이고 뒤가 거짓일 때만 거짓이고, 나머지 세 경우에는 참이다.

입력은 여러 개의 테스트 케이스로 이루어진다.

각 테스트 케이스는 가정 논리식의 개수 N (0 < N < 500)으로 시작한다. 이어지는 N개의 줄에 논리식이 한 줄에 하나씩 주어지며, 문법은 다음과 같다.

Statement:   Variable | Negation | (Implication)
Variable:    a,b,c,d,...,t
Implication: Statement->Statement
Negation:    ~(Statement)

변수는 소문자 a부터 t까지 20개다. 부정은 항상 괄호를 동반해 ~(...) 꼴로 쓰고, 함의는 항상 (...->...) 꼴로 괄호에 싸여 있다. 논리식 안에는 공백이 없다. 이 N개의 논리식은 모두 참이라고 가정한다.

그다음 줄에 질의 논리식의 개수 M (0 < M < 500)이 주어지고, 이어지는 M개의 줄에 질의 논리식이 한 줄에 하나씩 주어진다.

입력의 마지막 줄에는 0이 하나 주어진다.

각 테스트 케이스마다 먼저 ====를 한 줄에 출력한다.

이어서 M개의 질의 논리식을 주어진 순서대로 처리한다. 가정 N개를 모두 참으로 만드는 모든 진리값 배정에서 그 논리식이 참이면 True를, 그렇지 않은 배정이 하나라도 있으면 False를 한 줄에 출력한다.

가정을 모두 참으로 만드는 배정이 하나도 없으면 M개의 답은 모두 True다.