반복 없는 논리식

Nick은 불 논리(Boolean logic)를 연구하며, 그의 전문 분야는 반복 없는 함수입니다. 어떤 불 함수가 반복 없는(read-once) 함수라는 것은, 모든 변수가 정확히 한 번씩만 나타나는 논리식으로 표현할 수 있다는 뜻입니다.

논리식의 문법은 다음과 같습니다.

• 변수 — 문자 a부터 k까지.
• 괄호 — E가 논리식이면 (E)도 논리식입니다.
• 부정 — 임의의 논리식 E에 대해 ~E는 논리식입니다.
• 논리곱(AND) — E1 & E2 & ... & En.
• 논리합(OR) — E1 | E2 | ... | En.

연산자의 우선순위는 높은 것부터 낮은 순서로 ~(NOT), &(AND), |(OR)입니다.

이러한 논리식으로 주어진 불 함수가 있습니다. 이 식에는 같은 변수가 여러 번 나올 수 있습니다. 이 식이 계산하는 함수가 반복 없는 함수인지 판정하고, 그렇다면 그 함수를 나타내는 반복 없는 논리식을 하나 출력하세요.

입력의 한 줄에 불 함수가 문자열로 주어집니다. 문자열은 a..k, (, ), 공백, ~, &, | 문자로 이루어지며, ~, &, |는 각각 NOT, AND, OR를 뜻합니다. 토큰 사이에는 공백이 몇 개든 올 수 있습니다. 줄의 길이는 최대 1000자이며, 주어지는 논리식은 문법적으로 올바릅니다.

함수가 반복 없는 함수가 아니면 No를 출력합니다. 상수 함수(항상 참 또는 항상 거짓)도 변수를 반복하지 않고는 표현할 수 없으므로 여기에 포함됩니다.

반복 없는 함수이면 첫 줄에 Yes를, 둘째 줄에는 아래 규칙으로 정의되는 정규(canonical) 반복 없는 논리식을 출력합니다. 한 함수에 대해 동치인 반복 없는 논리식이 여러 개일 수 있으므로, 정확히 하나의 정규형만을 정답으로 인정합니다.

• 함수가 실제로 의존하는 변수만 나타냅니다. 결과에 영향을 주지 않는 변수는 제거합니다(예: a | b & ~b는 a와 같습니다).
• 모든 부정은 변수 바로 앞으로 밀어 넣어, ~는 ~a처럼 변수 바로 앞에만 나타나게 합니다. ~(...) 형태는 쓰지 않습니다.
• 논리식은 단일 리터럴을 잎으로 하는 &, | 노드의 트리입니다. 같은 연산자가 인접하면 하나로 합쳐, & 노드는 & 자식을 갖지 않고 | 노드는 | 자식을 갖지 않습니다.
• 각 노드 안에서는 피연산자가 포함하는 변수 중 알파벳 순으로 가장 작은 변수를 기준으로 정렬합니다. 한 노드의 피연산자들은 서로 다른 변수를 쓰므로 이 순서는 유일합니다.
• 모든 이항 &와 |의 양옆에 공백을 정확히 하나씩 둡니다. 괄호는 우선순위상 필요한 곳에만 넣습니다. 즉 & 노드 바로 안에 있는 | 피연산자는 괄호로 감싸고, 그 밖에는 괄호를 넣지 않습니다.

출력하는 줄의 길이는 최대 1000자입니다.