항진식 판별

WFF 'N PROOF는 주사위로 하는 논리 게임입니다. 각 주사위의 여섯 면에는 기호 K, A, N, C, E, p, q, r, s, t 중 일부가 적혀 있습니다. 정형식(WFF, Well-formed Formula)은 다음 규칙을 따르는 기호 문자열입니다.

• p, q, r, s, t는 각각 WFF이다.
• w가 WFF이면 Nw도 WFF이다.
• w와 x가 WFF이면 Kwx, Awx, Cwx, Ewx도 WFF이다.

WFF의 의미는 다음과 같이 정의됩니다.

• p, q, r, s, t는 0(거짓) 또는 1(참) 값을 가질 수 있는 논리 변수입니다.
• K, A, N, C, E는 각각 그리고(and), 또는(or), 부정(not), 함의(implies), 동치(equals)를 의미하며, 아래 진리표로 정의됩니다.

항진식(tautology)은 변수 값에 관계없이 항상 1(참)이 되는 WFF입니다. 예를 들어 ApNp는 p의 값과 상관없이 참이므로 항진식입니다. 반면 ApNq는 p=0, q=1일 때 값이 0이 되므로 항진식이 아닙니다.

주어진 WFF가 항진식인지 아닌지 판별하세요.

입력은 여러 개의 테스트 케이스로 이루어집니다. 각 테스트 케이스는 기호가 100개 이하인 WFF 하나가 적힌 한 줄입니다. 마지막 케이스 다음 줄에는 0만 적힌 줄이 옵니다.

각 테스트 케이스마다 항진식이면 tautology, 아니면 not을 한 줄에 출력하세요.