WFF 'N PROOF

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)을 의미하며, 그 정의는 아래 진리표와 같습니다.

주사위를 던져 얻은 기호들의 모음이 주어질 때, 그 기호 중 일부를 사용해 만들 수 있는 가장 긴 WFF의 길이를 구하세요.

입력은 여러 개의 테스트 케이스로 이루어집니다. 각 테스트 케이스는 K, A, N, C, E, p, q, r, s, t 문자로 이루어진 길이 1 이상 100 이하의 문자열이 한 줄에 주어집니다. 마지막 테스트 케이스 다음에는 0 하나만 있는 줄이 옵니다.

각 테스트 케이스마다, 문자열의 문자 중 일부를 사용해 만들 수 있는 가장 긴 WFF의 길이를 한 줄에 출력합니다. WFF를 하나도 만들 수 없으면 no WFF possible이라고 적힌 줄을 출력합니다.