E

E. Проверка доказательства в формальной арифметике

Имя входного файла:                 стандартный ввод
Имя выходного файла:                стандартный вывод
Ограничение по времени:             1 секунда
Ограничение по памяти:              256 мегабайт

Напишите программу, проверяющую доказательство в формальной арифметике на корректность. Докзательство соответствует следующей грамматике.

      ⟨ВВод⟩ ::= ⟨Заголовок⟩`\n'⟨Доказательство⟩
 ⟨Заголовок⟩ ::= [{⟨Выражение⟩`,'}*⟨Выражение⟩] `|-'⟨Выражение⟩
 ⟨Выражение⟩ ::= ⟨Дизъюнкция⟩|⟨Дизъюнкция⟩`->'⟨Выражение⟩
⟨Дизъюнкция⟩ ::= ⟨Конъюнкция⟩|⟨Дизъюнкция⟩`|'⟨Конъюнкция⟩
⟨Конъюнкция⟩ ::= ⟨Отрицание⟩|⟨Конъюнкция⟩`&'⟨Унарное⟩
   ⟨Унарное⟩ ::= ⟨Предикат⟩| `!'⟨Унарное⟩| `('⟨Выражение⟩`)'
              | (`@'|`?')⟨Переменная⟩`.'⟨Выражение⟩
⟨Переменная⟩ ::= (`A'...`Z'){`A'...`Z'|`0'...`9'|`''}*
⟨Переменная⟩ ::= (`a'...`z') {`0'...`9'}*
  ⟨Предикат⟩ ::= (`A'...`Z') {`0'...`9'}*[`('⟨Терм⟩{`,'⟨Терм⟩}*`)']
              | ⟨Терм⟩`='⟨Терм⟩
      ⟨Терм⟩ ::= ⟨Слагаемое⟩|⟨Терм⟩`+'⟨Слагаемое⟩
 ⟨Слагаемое⟩ ::= ⟨Умножаемое⟩|⟨Слагаемое⟩`*'⟨Умножаемое⟩
⟨Умножаемое⟩ ::= (`a'... `z') {`0'...`9'}*`('⟨Терм⟩{`,'⟨Терм⟩}*`)'
              | ⟨Переменная⟩| `('⟨Терм⟩`)'
              | ` 0 ' |⟨Умножаемое⟩`''

Формат входных данных

Доказательство.

Формат выходных данных

Если доказательство корректно, выведите «Proof is correct». Если в доказательстве нет ошибок, 
но требуемое выражение не доказано, выведите «Required hasn't been proven». Иначе, выведите 
«Line #x can't be obtained», где x — номер первого некорректной строки в доказательстве.
Строки доказательства нумеруются с 1.